Definition left_strength_laws {F : V ⟶ V} (tF : left_strength_data F) : UU := (∏ (x₁ x₂ y₁ y₂ : V) (f : x₁ --> x₂) (g : y₁ --> y₂), f #⊗ #F g· tF x₂ y₂ = tF x₁ y₁ · #F(f #⊗ g)) × (∏ (x : V), tF I_{V} x · #F(mon_lunitor x) = mon_lunitor (F x)) × (∏ (x y z : V), tF (x ⊗ y) z · #F(mon_lassociator x y z) = mon_lassociator x y (F z) · identity x #⊗ tF y z · tF x (y ⊗ z)).
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.Monads.Monads. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import MonoidalNotations.