proposition: Lemma setofendabgr_un0 {G: abgr} : monoidfun G G.
proof: Proof. apply (@monoidfunconstr _ _ (λ x : G, 0)). apply make_dirprod. - intros x x'. rewrite (lunax G). reflexivity. - reflexivity. Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids