fact: Definition setofendabgr (G : abgr) : hSet := make_hSet (monoidfun G G) (isasetmonoidfun G G).
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids