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. induction p, q ; 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.