proposition: Lemma tensorialstrength_lineator_nat_left {C : category} (M : monoidal C) {F : functor C C} (ts : tensorialstrength M F) : lineator_nat_left _ _ _ _ ts = ∏ (v x1 x2 : C) (g : C ⟦ x1, x2 ⟧), v ⊗^{ M}_{l} # F g · ts v x2 = ts v x1 · # F (v ⊗^{ M}_{l} g).
proof: Proof. apply idpath. 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