proposition: 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: 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.
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