Lemma lineator_preservesactorinv (ll : lineator_lax) : preserves_actorinv ll. Proof. intros v w x. rewrite assoc'. apply (z_iso_inv_on_right _ _ _ (z_iso_from_actor_iso Mon_V ActD _ _ _)). cbn. etrans. 2: { repeat rewrite assoc. apply cancel_postcomposition. apply lineator_preservesactor. } repeat rewrite assoc'. etrans. { apply pathsinv0, id_right. } apply maponpaths. etrans. 2: { rewrite <- functor_comp. apply maponpaths. apply pathsinv0, (actegory_actorisolaw Mon_V ActC). } apply pathsinv0, functor_id. 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.