Lemma abgrfuntounit_ismonoidfun (X : abgr) : ismonoidfun (Y := unitabgr) (λ x : X, 0). Proof. use make_ismonoidfun. - use make_isbinopfun. intros x x'. use isProofIrrelevantUnit. - use isProofIrrelevantUnit. Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.