Definition to_iso_twosided_disp_profunctor : is_iso_twosided_disp (D := twosided_disp_cat_of_profunctors) (identity_is_z_iso _) (identity_is_z_iso _) τ. Proof. refine (inv_square_profunctor ,, _ ,, _). - abstract (use eq_profunctor_square ; intros y x h ; cbn ; refine (homotinvweqweq (make_weq _ (Hτ _ _)) _ @ _) ; refine (!_) ; exact (transportf_disp_mor2_profunctors (!(id_left (C := cat_of_setcategory) (functor_identity _))) (!(id_left (C := cat_of_setcategory) (functor_identity _))) (id_h_profunctor_square P) h)). - abstract (use eq_profunctor_square ; intros y x h ; cbn ; refine (homotweqinvweq (make_weq _ (Hτ _ _)) _ @ _) ; refine (!_) ; exact (transportf_disp_mor2_profunctors (!(id_left (C := cat_of_setcategory) (functor_identity _))) (!(id_left (C := cat_of_setcategory) (functor_identity _))) (id_h_profunctor_square Q) h)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Profunctors.Examples. Require Import UniMath.CategoryTheory.Profunctors.Transformation. Require Import UniMath.CategoryTheory.Profunctors.Squares. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Section FromProfunctorIso. End FromProfunctorIso.