proposition: Lemma preserves_tensorinv_nat_left {C D : category} {M : monoidal C} {N : monoidal D} {F : functor C D} {pt : preserves_tensordata M N F} (pts : preserves_tensor_strongly pt) (ptrn : preserves_tensor_nat_left pt) (x1 x2 y : C) (f : C⟦x1,x2⟧) : (is_z_isomorphism_mor (pts y x1)) · F y ⊗^{ N}_{l} # F f = # F (y ⊗^{ M}_{l} f) · (is_z_isomorphism_mor (pts y x2)).
proof: Proof. set (ptiso := pt y x1 ,, pts y x1 : z_iso _ _). apply (z_iso_inv_on_right _ _ _ ptiso). rewrite assoc. etrans. 2: { apply maponpaths_2. apply ptrn. } rewrite assoc'. unfold is_z_isomorphism_mor. rewrite (pr12 (pts y x2)). apply (! id_right _). 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