proposition: 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: 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.
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