proposition: Proposition transportb_prebicat_twosided_disp_cat {C₁ C₂ : bicat_of_univ_cats} {F G : C₁ --> C₂} {τ θ : F ==> G} (p : τ = θ) {D₁ : disp_prebicat_data_twosided_disp_cat C₁} {D₂ : disp_prebicat_data_twosided_disp_cat C₂} {FF : D₁ -->[ F ] D₂} {GG : D₁ -->[ G ] D₂} (θθ : FF ==>[ θ ] GG) (x y : pr11 C₁) (xy : pr11 D₁ x y) : pr1 (transportb (λ z, FF ==>[ z ] GG) p θθ) x y xy = transportb_disp_mor2 (maponpaths (λ n, pr1 n x) p) (maponpaths (λ n, pr1 n y) p) (pr1 θθ x y xy).
proof: Proof. induction p. cbn. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfDispCats UniMath.Bicategories.DisplayedBicats.UnivalenceTechniques UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.CatDiag UniMath.Bicategories.DisplayedBicats.DispPseudofunctor