proposition: Lemma disp_mor_transportf_prewhisker_gen (a b : C) {x y z : C⟦a,b⟧} {f : x ==> y} {A : UU} {t : A → y ==> z} {g g' : A} (ef : g = g') {aa : D a} {bb : D b} {xx : aa -->[x] bb} {yy} {zz} (ff : xx ==>[f] yy) (gg : yy ==>[t g] zz) : ff •• (transportf (λ x, _ ==>[t x] _) ef gg) = transportf (λ x, _ ==>[x] _) (maponpaths (λ h, f • t h) ef) (ff •• gg).
proof: Proof. induction ef; apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Univalence