proposition: Lemma ismonoidfuncomp {X Y Z : monoid} (f : monoidfun X Y) (g : monoidfun Y Z) : ismonoidfun (funcomp (pr1 f) (pr1 g)).
proof: Proof. split with (isbinopfuncomp f g). simpl. rewrite (pr2 (pr2 f)). apply (pr2 (pr2 g)). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders