Lemma comp_lineator_laxlaws : lineator_laxlaws comp_lineator_data. Proof. split4; intro; unfold comp_lineator_data; intros; cbn. - etrans. 2: { rewrite assoc'. apply maponpaths. apply functor_comp. } etrans. 2: { do 2 apply maponpaths. apply lineator_linnatleft. } rewrite functor_comp. repeat rewrite assoc. apply cancel_postcomposition. apply lineator_linnatleft. - etrans. 2: { rewrite assoc'. apply maponpaths. apply functor_comp. } etrans. 2: { do 2 apply maponpaths. apply lineator_linnatright. } rewrite functor_comp. repeat rewrite assoc. apply cancel_postcomposition. apply lineator_linnatright. - assert (auxF := lineator_preservesactor Fl v w x). assert (auxG := lineator_preservesactor Gl v w (F x)). rewrite (bifunctor_leftcomp ActE). etrans. 2: { repeat rewrite assoc. apply cancel_postcomposition. repeat rewrite assoc'. do 2 apply maponpaths. apply pathsinv0, lineator_linnatleft. } etrans. 2: { apply cancel_postcomposition. repeat rewrite assoc. apply cancel_postcomposition. exact auxG. } repeat rewrite assoc'. apply maponpaths. repeat rewrite <- functor_comp. apply maponpaths. etrans; [ exact auxF |]. apply assoc'. - assert (auxF := lineator_preservesunitor Fl x). assert (auxG := lineator_preservesunitor Gl (F x)). etrans; [| exact auxG]. clear auxG. rewrite <- auxF. clear auxF. repeat rewrite assoc'. apply maponpaths. apply pathsinv0, functor_comp. 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.