Lemma abmonoidshomabmonoid_ismonoidop (X Y : abmonoid) : @ismonoidop (make_hSet (monoidfun X Y) (isasetmonoidfun X Y)) (λ f g : monoidfun X Y, abmonoidshombinop f g). Proof. use make_ismonoidop. - intros f g h. exact (abmonoidshombinop_assoc f g h). - use make_isunital. + exact (unelmonoidfun X Y). + use make_isunit. * intros f. exact (abmonoidsbinop_lunax f). * intros f. exact (abmonoidsbinop_runax f). Defined.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.