Definition leftunitor_naturality {C : category} {T : tensor_data C} {I : C} (lu : leftunitor_data T I) : UU := ∏ (x y : C), ∏ (f : C ⟦x,y⟧), f∘(lu x) = (lu y)∘((identity I)⊗^{T}f).
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos.