Definition wtensor_to_ctensor (T : wtensor C) : ctensor C. Proof. repeat (use tpair). - apply T. - intros x1 x2 y1 y2 f g. exact (f ⊗^{T} g). - intros x y. apply (bifunctor_distributes_over_id (C := C) (bifunctor_leftid T) (bifunctor_rightid T) ). - intros x1 x2 x3 y1 y2 y3 f1 f2 g1 g2. apply (bifunctor_distributes_over_comp (C := C) (bifunctor_leftcomp T) (bifunctor_rightcomp T) (bifunctor_equalwhiskers T) ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Import BifunctorNotations.