proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.Core.Univalence UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories