proposition: Lemma lineatorinv_nat_left {ld : lineator_data} (ls : lineator_strongly ld) (lln : lineator_nat_left ld) (v : V) (x1 x2 : C) (f : C⟦x1,x2⟧) : (is_z_isomorphism_mor (ls v x1)) · v ⊗^{ActD}_{l} # F f = # F (v ⊗^{ActC}_{l} f) · (is_z_isomorphism_mor (ls v x2)).
proof: Proof. set (ldiso := ld v x1 ,, ls v x1 : z_iso _ _). apply (z_iso_inv_on_right _ _ _ ldiso). rewrite assoc. etrans. 2: { apply maponpaths_2. apply lln. } rewrite assoc'. unfold is_z_isomorphism_mor. rewrite (pr12 (ls v 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.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