fact: Definition submonoid_incl {X : monoid} (A : submonoid X) : monoidfun A X := monoidfunconstr (ismonoidfun_pr1 A).
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders