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