Lemma preserves_actor_of_inverse_lineator_strongly {ld : lineator_data} (pα : preserves_actor ld) (ls : lineator_strongly ld) (v w : V) (x : C) : (is_z_isomorphism_mor (ls (v ⊗_{Mon_V} w) x)) · aα^{ActD}_{v, w, F x} = (#F (aα^{ActC}_{v,w,x})) · (is_z_isomorphism_mor (ls v (w ⊗_{ActC} x))) · (v ⊗^{ActD}_{l} (is_z_isomorphism_mor (ls w x))). Proof. set (lsv_wx := pointwise_z_iso_from_lineator_strongly ls v (w ⊗_{ActC} x)). set (lsvw_x := pointwise_z_iso_from_lineator_strongly ls (v ⊗_{Mon_V} w) x). set (lsfv := functor_on_z_iso (leftwhiskering_functor ActD v) (pointwise_z_iso_from_lineator_strongly ls w x)). apply (z_iso_inv_on_left _ _ _ _ lsfv). apply pathsinv0. apply (z_iso_inv_on_left _ _ _ _ lsv_wx). rewrite assoc'. rewrite assoc'. etrans. 2: { apply maponpaths. rewrite assoc. exact (pα v w x). } etrans. 2: { rewrite assoc. apply maponpaths_2. exact (! pr222 lsvw_x). } 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.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.ConstructionOfActegories. Require Import UniMath.CategoryTheory.coslicecat. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects. Import BifunctorNotations. Import MonoidalNotations. Import ActegoryNotations.