proposition: Lemma abmonoidshomabmonoid_ismonoidop (X Y : abmonoid) : @ismonoidop (make_hSet (monoidfun X Y) (isasetmonoidfun X Y)) (λ f g : monoidfun X Y, abmonoidshombinop f g).
proof: 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.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders