Definition triangle_identity {C : category} {T : tensor_data C} {I : C} (lu : leftunitor_data T I) (ru : rightunitor_data T I) (α : associator_data T) := ∏ (x y : C), (((identity x) ⊗^{T} (lu y) ) ∘ (α x I y)) = ((ru x) ⊗^{T} identity y).
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos.