fact: Definition post_whisker_disp_nat_trans {C₁ C₂ C₃ : category} {F₁ F₂ : C₁ ⟶ C₂} {n : F₁ ⟹ F₂} {G : C₂ ⟶ C₃} {D₁ : disp_cat C₁} {D₂ : disp_cat C₂} {D₃ : disp_cat C₃} {FF₁ : disp_functor F₁ D₁ D₂} {FF₂ : disp_functor F₂ D₁ D₂} (nn : disp_nat_trans n FF₁ FF₂) (GG : disp_functor G D₂ D₃) : disp_nat_trans (post_whisker n G) (disp_functor_composite FF₁ GG) (disp_functor_composite FF₂ GG).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Isos