Definition iso_twosided_disp_profunctor_weq {C D : setcategory} (P Q : C ↛ D) : profunctor_iso_square (functor_identity _) (functor_identity _) P Q ≃ iso_twosided_disp (D := twosided_disp_cat_of_profunctors) (identity_z_iso _) (identity_z_iso _) P Q. Proof. use weqfibtototal. intro τ. use weqimplimpl. - apply to_iso_twosided_disp_profunctor. - intros H y x. exact (from_iso_twosided_disp_profunctor H y x). - apply isaprop_is_profunctor_nat_iso. - apply isaprop_is_iso_twosided_disp. 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.