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