Proposition transportf_disp_mor2_profunctors {C₁ C₂ D₁ D₂ : cat_of_setcategory} {P : twosided_disp_cat_of_profunctors_data C₁ D₁} {Q : twosided_disp_cat_of_profunctors_data C₂ D₂} {FD : functor_data (C₁ : setcategory) (C₂ : setcategory)} {HF₁ HF₂ : is_functor FD} (F₁ := make_functor FD HF₁) (F₂ := make_functor FD HF₂) (p : F₁ = F₂) {GD : functor_data (D₁ : setcategory) (D₂ : setcategory)} {HG₁ HG₂ : is_functor GD} (G₁ := make_functor GD HG₁) (G₂ := make_functor GD HG₂) (q : G₁ = G₂) (τ : P -->[ F₁ ][ G₁] Q) {y : (D₁ : setcategory)} {x : (C₁ : setcategory)} (h : (P : profunctor _ _) y x) : (@transportf_disp_mor2 _ _ (twosided_disp_cat_of_profunctors_data) C₁ C₂ D₁ D₂ P Q F₁ F₂ p G₁ G₂ q τ : profunctor_square _ _ _ _) y x h = (τ : profunctor_square _ _ _ _) y x h. Proof. rewrite transportf_disp_mor2_profunctors_help. cbn. assert (path_functor_ob q y = idpath _) as r. { apply isaset_ob. } rewrite r ; clear r. assert (path_functor_ob p x = idpath _) as r. { apply isaset_ob. } rewrite r ; clear r. cbn. apply idpath. 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.