Lemma is_linear_nat_trans_comp {F G H : functor C D} (Fl : lineator_lax Mon_V ActC ActD F) (Gl : lineator_lax Mon_V ActC ActD G) (Hl : lineator_lax Mon_V ActC ActD H) {ξ1 : F ⟹ G} {ξ2 : G ⟹ H} (islnt1 : is_linear_nat_trans Fl Gl ξ1) (islnt2 : is_linear_nat_trans Gl Hl ξ2) : is_linear_nat_trans Fl Hl (nat_trans_comp _ _ _ ξ1 ξ2). Proof. intros v x. cbn. rewrite (bifunctor_leftcomp ActD). rewrite assoc. etrans. { apply cancel_postcomposition. apply islnt1. } do 2 rewrite assoc'. apply maponpaths. apply islnt2. 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.