proposition: Lemma abgrshomabgr_isabgrop (X Y : abgr) : @isabgrop (abmonoidshomabmonoid X Y) (λ f g : monoidfun X Y, @abmonoidshombinop X Y f g).
proof: Proof. use make_isabgrop. - use make_isgrop. + exact (abmonoidshomabmonoid_ismonoidop X Y). + use make_invstruct. * intros f. exact (abgrshombinop_inv f). * use make_isinv. intros f. exact (abgrshombinop_linvax f). intros f. exact (abgrshombinop_rinvax f). - intros f g. exact (abmonoidshombinop_comm f g). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids