proposition: Lemma grfunfromunit_ismonoidfun (X : gr) : ismonoidfun (λ x : unitgr, (unel X)).
proof: Proof. use make_ismonoidfun. - use make_isbinopfun. intros x x'. use pathsinv0. use (runax X). - use idpath. Qed.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids