Lemma disp_eq_to_tensoriso {C : bicat_of_univ_cats} (TC TD : bidisp_tensor_disp_bicat C) : disp_adjoint_equivalence (idtoiso_2_0 C C (idpath C)) TC TD -> tensor_iso TC TD. Proof. intro dae. induction dae as [[ptd ptnat] [data [ax equiv]]]. induction data as [ptdinv [ptunit ptcounit]]. cbn in *. use tpair. - intros x y. use make_z_iso. + exact (ptd x y). + exact (pr1 ptdinv x y). + split. * set (t := ptcounit x y). cbn in t. unfold identityfunctor_preserves_tensor_data in t. rewrite id_right in t. rewrite tensor_id in t. rewrite id_right in t. unfold compositions_preserves_tensor_data in t. unfold functor_identity in t. exact t. * set (t := ! ptunit x y). cbn in t. unfold identityfunctor_preserves_tensor_data in t. rewrite id_left in t. rewrite tensor_id in t. rewrite id_left in t. unfold compositions_preserves_tensor_data in t. exact t. - intros x1 x2 y1 y2 f g. exact (ptnat x1 x2 y1 y2 f 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.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Import TensorNotation. Import TensorNotation.