Definition monoid_precategory_data : precategory_data := make_precategory_data monoid_precategory_ob_mor (λ (X : monoid), ((idmonoidiso X) : monoidfun X X)) (fun (X Y Z : monoid) (f : monoidfun X Y) (g : monoidfun Y Z) => monoidfuncomp f g). Local Lemma monoid_id_left {X Y : monoid} (f : monoidfun X Y) : monoidfuncomp (idmonoidiso X) f = f. Proof. use monoidfun_paths. use idpath. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Free_Monoids_and_Groups. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Adjunctions.Core.