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).
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.