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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import BifunctorNotations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.