Definition from_iso_twosided_disp_profunctor (y : D) (x : C) : isweq (τ y x). Proof. use isweq_iso. - exact (θ y x). - abstract (intros h ; refine (profunctor_square_eq_pointwise (inv_after_iso_twosided_disp Hτ) h @ _) ; 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 (intros h ; refine (profunctor_square_eq_pointwise (iso_after_inv_twosided_disp Hτ) h @ _) ; 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.