Definition tensor_on_hom {C : category} (T : tensor_data C) : ∏ (x1 x2 y1 y2 : C), C⟦x1,x2⟧ -> C⟦y1,y2⟧ -> C⟦x1 ⊗_{T} y1, x2 ⊗_{T} y2⟧ := pr2 T.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Import TensorNotation. Import TensorUnitNotation. Import TensorNotation. Import TensorUnitNotation. Import TensorNotation. Import TensorUnitNotation. Import TensorNotation. Import TensorUnitNotation. Import UnitorsAssociatorNotation. Import TensorNotation. Import TensorUnitNotation. Import UnitorsAssociatorNotation.