proposition: Lemma lineator_preservesunitorinv (ll : lineator_lax) : preserves_unitorinv ll.
proof: Proof. intro x. apply (z_iso_inv_on_right _ _ _ (_,,_,, actegory_unitorisolaw Mon_V ActD (F x))). cbn. rewrite <- (lineator_preservesunitor ll). repeat rewrite assoc'. etrans. { apply pathsinv0, id_right. } apply maponpaths. etrans. 2: { rewrite <- functor_comp. apply maponpaths. apply pathsinv0, (actegory_unitorisolaw Mon_V ActC x). } apply pathsinv0, functor_id. 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