proposition: Lemma abmonoidfunfromunit_ismonoidfun (X : abmonoid) : ismonoidfun (λ x : unitabmonoid, (unel X)).
proof: Proof. use make_ismonoidfun. - use make_isbinopfun. intros x x'. use pathsinv0. use (runax X). - use idpath. Qed.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders