Lemma grfuntounit_ismonoidfun (X : gr) : ismonoidfun (Y := unitgr) (λ x : X, 1). Proof. use make_ismonoidfun. - use make_isbinopfun. intros x x'. use isProofIrrelevantUnit. - use isProofIrrelevantUnit. Qed.
Require Import UniMath.MoreFoundations.Subtypes.