Proposition twosided_disp_cat_of_profunctors_axioms : twosided_disp_cat_axioms twosided_disp_cat_of_profunctors_data. Proof. repeat split. - intros C₁ C₂ D₁ D₂ P Q F G τ. use eq_profunctor_square. intros y x h ; cbn. refine (!_). apply transportf_disp_mor2_profunctors. - intros C₁ C₂ D₁ D₂ P Q F G τ. use eq_profunctor_square. intros y x h ; cbn. refine (!_). exact (transportf_disp_mor2_profunctors (!(id_right F)) (!(id_right G)) τ h). - intros C₁ C₂ C₃ C₄ D₁ D₂ D₃ D₄ P₁ P₂ P₃ P₄ F₁ F₂ F₃ G₁ G₂ G₃ τ₁ τ₂ τ₃. use eq_profunctor_square. intros y x h ; cbn. refine (!_). exact (transportf_disp_mor2_profunctors (!(assoc F₁ F₂ F₃)) (!(assoc G₁ G₂ G₃)) (comp_h_profunctor_square (comp_h_profunctor_square τ₁ τ₂) τ₃) h). - intro ; intros. apply isaset_profunctor_square. Qed.
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.