Definition tensoriso_to_disp_eq {C : bicat_of_univ_cats} (TC TD : bidisp_tensor_disp_bicat C) : tensor_iso TC TD -> disp_adjoint_equivalence (idtoiso_2_0 C C (idpath C)) TC TD. Proof. intro ti. use tpair. - use tpair. + intros x y. apply ti. + intros x1 x2 y1 y2 f g. exact ((pr2 ti) x1 x2 y1 y2 f g). - use tpair. + repeat (use tpair). * intros x y. apply ti. * intros x1 x2 y1 y2 f g. induction ti as [n i]. apply (swap_along_zisos (n x1 y1) (n x2 y2) (f ⊗^{pr1 TD} g) (f ⊗^{pr1 TC} g)). exact (i x1 x2 y1 y2 f g). * intros x y. cbn. unfold identityfunctor_preserves_tensor_data. unfold compositions_preserves_tensor_data. rewrite id_left. rewrite tensor_id. rewrite id_left. apply (! z_iso_after_z_iso_inv ((pr1 ti x y))). * intros x y. cbn. unfold compositions_preserves_tensor_data. unfold identityfunctor_preserves_tensor_data. rewrite id_right. rewrite tensor_id. rewrite id_left. cbn. apply (z_iso_inv_after_z_iso ((pr1 ti x y))). + split. * split. -- abstract (repeat (apply funextsec ; intro) ; apply univalent_category_has_homsets). -- apply funextsec ; intro ; apply funextsec ; intro. apply univalent_category_has_homsets. * split. -- use tpair. ++ intros x y. cbn. unfold compositions_preserves_tensor_data. unfold identityfunctor_preserves_tensor_data. cbn. rewrite id_right. rewrite id_right. rewrite tensor_id. apply (z_iso_after_z_iso_inv ((pr1 ti x y))). ++ split. ** abstract (repeat (apply funextsec ; intro) ; apply univalent_category_has_homsets). ** abstract (repeat (apply funextsec ; intro) ; apply univalent_category_has_homsets). -- use tpair. ++ intros x y. cbn. unfold compositions_preserves_tensor_data. unfold identityfunctor_preserves_tensor_data. cbn. rewrite id_right. rewrite tensor_id. rewrite id_left. apply (! z_iso_inv_after_z_iso ((pr1 ti x y))). ++ split. ** abstract (repeat (apply funextsec ; intro) ; apply univalent_category_has_homsets). ** abstract (repeat (apply funextsec ; intro) ; apply univalent_category_has_homsets). 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.