Definition setofendabgr_inv {G : abgr} : monoidfun G G -> monoidfun G G. Proof. intro f. apply (@monoidfunconstr G G (λ x : G, grinv G (pr1setofendabgr f x))). apply make_dirprod. - intros x x'. rewrite (setofendabgr_to_isbinopfun f). rewrite (grinvop G). apply (commax G). - rewrite (setofendabgr_to_unel f). apply (grinvunel G). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids.