proposition: Lemma comp_is_monoid_mor {x y z : C} {f : C ⟦ x, y ⟧} {g : C ⟦ y, z ⟧} {xx : monoid x} {yy : monoid y} {zz : monoid z} (pf : is_monoid_mor xx yy f) (pg : is_monoid_mor yy zz g) : is_monoid_mor xx zz (f · g).
proof: Proof. split. - etrans. { apply maponpaths_2. apply bifunctor_distributes_over_comp. apply (bifunctor_leftcomp M). apply (bifunctor_rightcomp M). apply (bifunctor_equalwhiskers M). } etrans. 1: apply assoc'. etrans. 1: apply maponpaths, (pr1 pg). etrans. 1: apply assoc. etrans. 1: apply maponpaths_2, (pr1 pf). apply assoc'. - unfold is_monoid_mor_unit. etrans. 1: apply assoc. etrans. 1: apply maponpaths_2, (pr2 pf). apply (pr2 pg). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total