proposition: Lemma is_linear_nat_trans_identity {F : functor C D} (Fl : lineator_lax Mon_V ActC ActD F) : is_linear_nat_trans Fl Fl (nat_trans_id F).
proof: Proof. intros v c. rewrite id_right. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, (bifunctor_leftid ActD). } apply pathsinv0, id_left. 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