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. 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.
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.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import BifunctorNotations. Import MonoidalNotations.