fact: Definition transportf_postwhisker_1cell {B : bicat} {D : disp_bicat B} {x y z : B} {xx : D x} {yy : D y} {zz : D z} {f : x --> y} {g₁ g₂ : y --> z} (p : g₁ = g₂) (ff : xx -->[ f ] yy) (gg : yy -->[ g₁ ] zz) : (ff ;; transportf (λ z, yy -->[ z ] zz) p 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