Lemma grfunfromunit_ismonoidfun (X : gr) : ismonoidfun (Y := X) (λ x : unitgr, 1). Proof. use make_ismonoidfun. - use make_isbinopfun. intros x x'. exact (!runax X _). - use idpath. Qed.
Require Import UniMath.MoreFoundations.Subtypes.