Definition totalcategory_tensordata : tensor_data ToD. Proof. use tpair. + intros xa yb. exact ((pr1 xa) ⊗_{T} (pr1 yb) ,, (pr2 xa) ⊗_{{dtd}} (pr2 yb)). + intros xa yb xa' yb' f g. split with (pr1 f ⊗^{T} pr1 g). apply (pr2 dtd). - exact (pr2 f). - exact (pr2 g). Defined.
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.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.DisplayedMonoidalCurried. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsCurried. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total.