proposition: Proposition transportf_disp_mor2_profunctors_help {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₂} {F₁ F₂ : (C₁ : setcategory) ⟶ (C₂ : setcategory)} (p : F₁ = F₂) {G₁ G₂ : (D₁ : setcategory) ⟶ (D₂ : setcategory)} (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 = transportf (λ z, (Q : _ ↛ _) z _) (path_functor_ob q y) (transportf (λ z, (Q : _ ↛ _) _ z) (path_functor_ob p x) ((τ : profunctor_square _ _ _ _) y x h)).
proof: Proof. induction p, q ; 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