proposition: Proposition twosided_disp_cat_of_profunctors_axioms : twosided_disp_cat_axioms twosided_disp_cat_of_profunctors_data.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Categories.CategoryOfSetCategories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.Profunctors.Core UniMath.CategoryTheory.Profunctors.Examples UniMath.CategoryTheory.Profunctors.Transformation UniMath.CategoryTheory.Profunctors.Squares UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence