proposition: 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: 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.
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.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.ConstructionOfActegories UniMath.CategoryTheory.coslicecat UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects