Lemma lineatorinv_nat_right {ld : lineator_data} (ls : lineator_strongly ld) (lrn : lineator_nat_right ld) (v1 v2 : V) (x : C) (f : V⟦v1,v2⟧) : (is_z_isomorphism_mor (ls v1 x)) · f ⊗^{ActD}_{r} F x = #F (f ⊗^{ActC}_{r} x) · (is_z_isomorphism_mor (ls v2 x)). Proof. set (ldiso := ld v1 x ,, ls v1 x : z_iso _ _). apply (z_iso_inv_on_right _ _ _ ldiso). rewrite assoc. etrans. 2: { apply maponpaths_2. apply lrn. } rewrite assoc'. unfold is_z_isomorphism_mor. rewrite (pr12 (ls v2 x)). apply (! id_right _). 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.