Lemma ismonoidfuncomp {X Y Z : monoid} (f : monoidfun X Y) (g : monoidfun Y Z) : ismonoidfun (g ∘ f). Proof. exists (isbinopfuncomp f g). simpl. rewrite (pr2 (pr2 f)). apply (pr2 (pr2 g)). Qed.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.