Lemma comp_fmonoidal_laxlaws {C D E : category} {M : monoidal C} {N : monoidal D} {O : monoidal E} {F : C ⟶ D} {G : D ⟶ E} (Fm : fmonoidal_lax M N F) (Gm : fmonoidal_lax N O G) : fmonoidal_laxlaws (comp_fmonoidal_data Fm Gm). Proof. repeat split; red; cbn; unfold fmonoidal_preservesunit, fmonoidal_preservestensordata; cbn; intros. - etrans. 2: { rewrite assoc'. apply maponpaths. apply functor_comp. } etrans. 2: { do 2 apply maponpaths. apply fmonoidal_preservestensornatleft. } rewrite functor_comp. repeat rewrite assoc. apply cancel_postcomposition. apply fmonoidal_preservestensornatleft. - etrans. 2: { rewrite assoc'. apply maponpaths. apply functor_comp. } etrans. 2: { do 2 apply maponpaths. apply fmonoidal_preservestensornatright. } rewrite functor_comp. repeat rewrite assoc. apply cancel_postcomposition. apply fmonoidal_preservestensornatright. - assert (auxF := fmonoidal_preservesassociativity Fm x y z). unfold fmonoidal_preservestensordata in auxF. assert (auxG := fmonoidal_preservesassociativity Gm (F x) (F y) (F z)). unfold fmonoidal_preservestensordata in auxG. rewrite (bifunctor_leftcomp O). rewrite (bifunctor_rightcomp O). etrans. 2: { repeat rewrite assoc. apply cancel_postcomposition. repeat rewrite assoc'. do 2 apply maponpaths. apply pathsinv0, fmonoidal_preservestensornatleft. } etrans. 2: { apply cancel_postcomposition. repeat rewrite assoc. apply cancel_postcomposition. exact auxG. } repeat rewrite assoc'. apply maponpaths. etrans. 2: { apply maponpaths. rewrite <- functor_comp. apply functor_comp. } etrans. 2: { do 2 apply maponpaths. rewrite assoc. exact auxF. } do 2 rewrite functor_comp. repeat rewrite assoc. do 2 apply cancel_postcomposition. apply fmonoidal_preservestensornatright. - assert (auxF := fmonoidal_preservesleftunitality Fm x). assert (auxG := fmonoidal_preservesleftunitality Gm (F x)). unfold fmonoidal_preservesunit, fmonoidal_preservestensordata in auxF, auxG. etrans; [| exact auxG]. clear auxG. rewrite (bifunctor_rightcomp O). rewrite <- auxF. clear auxF. do 2 rewrite functor_comp. repeat rewrite assoc. do 2 apply cancel_postcomposition. repeat rewrite assoc'. apply maponpaths. apply fmonoidal_preservestensornatright. - assert (auxF := fmonoidal_preservesrightunitality Fm x). assert (auxG := fmonoidal_preservesrightunitality Gm (F x)). unfold fmonoidal_preservesunit, fmonoidal_preservestensordata in auxF, auxG. etrans; [| exact auxG]. clear auxG. rewrite (bifunctor_leftcomp O). rewrite <- auxF. clear auxF. do 2 rewrite functor_comp. repeat rewrite assoc. do 2 apply cancel_postcomposition. repeat rewrite assoc'. apply maponpaths. apply fmonoidal_preservestensornatleft. 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.