Definition ctensor_to_wtensor (T : ctensor C) : wtensor C. Proof. repeat (use tpair). - apply T. - intros x ? ? g. exact ((tensor_on_hom (pr1 T)) _ _ _ _ (identity x) g). - intros y ? ? f. exact ((tensor_on_hom (pr1 T)) _ _ _ _ f (identity y)). - intro ; intro. apply tensor_id. - intro ; intro. apply tensor_id. - intro ; intros. use pathscomp0. 3: apply tensor_comp. rewrite id_right. apply idpath. - intro ; intros. use pathscomp0. 3: apply tensor_comp. rewrite id_right. apply idpath. - intros ? ? ? ? f g. use pathscomp0. 3: apply tensor_comp. rewrite id_right. rewrite id_left. etrans. { apply (! tensor_comp _ _ _ _ _ _ _ _ _ _ _). } rewrite id_right. apply maponpaths. apply id_left. 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.