proposition: Lemma monoidfuntounit_ismonoidfun (X : monoid) : ismonoidfun (λ x : X, (unel unitmonoid)).
proof: Proof. use make_ismonoidfun. - use make_isbinopfun. intros x x'. use isProofIrrelevantUnit. - use isProofIrrelevantUnit. Qed.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders