proposition: Proposition is_symmetric_monoidal_comp {C D E : category} {M : monoidal C} {N : monoidal D} {O : monoidal E} {HM : symmetric M} {HN : symmetric N} {HO : symmetric O} {F : C ⟶ D} {G : D ⟶ E} {HF : fmonoidal_lax M N F} {HG : fmonoidal_lax N O G} (HHF : is_symmetric_monoidal_functor HM HN HF) (HHG : is_symmetric_monoidal_functor HN HO HG) : is_symmetric_monoidal_functor HM HO (comp_fmonoidal_lax HF HG).
proof: Proof. intros x y. cbn. rewrite !assoc. etrans. { apply maponpaths_2. apply HHG. } rewrite !assoc'. etrans. { apply maponpaths. rewrite <- functor_comp. apply maponpaths. apply HHF. } rewrite functor_comp. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric