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). Proof. use tpair. - exact (λ x xx, ♯ GG (nn x xx)). - abstract (intros x y f xx yy ff ; cbn ; rewrite <- !(disp_functor_comp_var GG) ; unfold transportb ; rewrite transport_f_f ; rewrite (disp_nat_trans_ax_var nn) ; rewrite disp_functor_transportf ; rewrite transport_f_f ; apply maponpaths_2 ; apply C₃). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.