proposition: Lemma comp_lineator_laxlaws : lineator_laxlaws comp_lineator_data.
proof: 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.
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