fact: Definition monoidmonocomp {X Y Z : monoid} (f : monoidmono X Y) (g : monoidmono Y Z) : monoidmono X Z := make_monoidmono (inclcomp (pr1 f) (pr1 g)) (ismonoidfuncomp f g).
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders