fact: Definition transportf_prewhisker_1cell {B : bicat} {D : disp_bicat B} {x y z : B} {xx : D x} {yy : D y} {zz : D z} {f₁ f₂ : x --> y} {g : y --> z} (p : f₁ = f₂) (ff : xx -->[ f₁ ] yy) (gg : yy -->[ g ] zz) : (transportf (λ z, xx -->[ z ] yy) p ff ;; gg = transportf (λ z, xx -->[ z ] zz) (maponpaths (λ z, z · _) p) (ff ;; gg))%mor_disp.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.DisplayedCats.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.DisplayedBicats.DispPseudofunctor