fact: Definition tensor_idax {C : category} (T : tensor_data C) := ∏ (x y : C), (identity x) ⊗^{T} (identity y) = identity (x ⊗_{T} y).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos