Lemma preserves_associativity_of_inverse_preserves_tensor {C D : category} {M : monoidal C} {N : monoidal D} {F : functor C D} {pt : preserves_tensordata M N F} (ptα : preserves_associativity pt) (pts : preserves_tensor_strongly pt) (x y z : C) : (is_z_isomorphism_mor (pts (x ⊗_{M} y) z)) · ((is_z_isomorphism_mor (pts x y)) ⊗^{N}_{r} (F z)) · α^{N}_{F x, F y, F z} = (#F (α^{M}_{x,y,z})) · (is_z_isomorphism_mor (pts x (y ⊗_{M} z))) · ((F x) ⊗^{N}_{l} (is_z_isomorphism_mor (pts y z))). Proof. set (ptsx_yz := pointwise_z_iso_from_preserves_tensor_strongly pts x (y ⊗_{M} z)). set (ptsxy_z := pointwise_z_iso_from_preserves_tensor_strongly pts (x ⊗_{M} y) z). set (ptsfx := functor_on_z_iso (leftwhiskering_functor N (F x)) (pointwise_z_iso_from_preserves_tensor_strongly pts y z)). set (ptsfz := functor_on_z_iso (rightwhiskering_functor N (F z)) (pointwise_z_iso_from_preserves_tensor_strongly pts x y)). apply (z_iso_inv_on_left _ _ _ _ ptsfx). apply pathsinv0. apply (z_iso_inv_on_left _ _ _ _ ptsx_yz). rewrite assoc'. rewrite assoc'. etrans. 2: { apply maponpaths. rewrite assoc. exact (ptα x y z). } etrans. 2: { rewrite assoc'. apply maponpaths. rewrite assoc. apply maponpaths_2. rewrite assoc. apply maponpaths_2. exact (! pr222 ptsfz). } rewrite id_left. etrans. 2: { rewrite assoc. apply maponpaths_2. exact (! pr222 ptsxy_z). } apply (! id_left _). 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.