Lemma abgrshomabgr_isabgrop (X Y : abgr) : @isabgrop (abmonoidshomabmonoid X Y) (λ f g : monoidfun X Y, @abmonoidshombinop X Y f g). 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.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.