fact: 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).
imports: UniMath.Foundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos