Definition tensor_compax {C : category} (T : tensor_data C) := ∏ (x1 x2 x3 y1 y2 y3 : C) (f1 : C⟦x1,x2⟧) (f2 : C⟦x2,x3⟧) (g1 : C⟦y1,y2⟧) (g2 : C⟦y2,y3⟧), (f1 · f2) ⊗^{T} (g1 · g2) = (f1 ⊗^{T} g1) · (f2 ⊗^{T} g2).
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.