Lemma comp_lineator_strongly_inverse_is_inverse (v : V) (x : C) : is_inverse_in_precat (comp_lineator_lax Fl Gl v x) (comp_lineator_strongly_inverse v x). Proof. split; cbn; unfold comp_lineator_data. - etrans. { repeat rewrite assoc'. apply maponpaths. unfold comp_lineator_strongly_inverse. rewrite assoc. apply cancel_postcomposition. rewrite <- functor_comp. apply maponpaths. apply (pr12 (lineator_linstrongly Fl v x)). } rewrite functor_id. rewrite id_left. apply (pr12 (lineator_linstrongly Gl v (F x))). - unfold comp_lineator_strongly_inverse. etrans. { repeat rewrite assoc'. apply maponpaths. rewrite assoc. apply cancel_postcomposition. apply (pr22 (lineator_linstrongly Gl v (F x))). } rewrite id_left. rewrite <- functor_comp. etrans. { apply maponpaths. apply (pr22 (lineator_linstrongly Fl v x)). } apply 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.