Lemma monoidfuntounit_ismonoidfun (X : monoid) : ismonoidfun (Y := unitmonoid) (λ x : X, 1). Proof. use make_ismonoidfun. - use make_isbinopfun. intros x x'. use isProofIrrelevantUnit. - use isProofIrrelevantUnit. Qed.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.