Definition post_whisker_twosided_disp_nat_trans : twosided_disp_nat_trans (post_whisker τ H : F ∙ H ⟹ F' ∙ H) (post_whisker θ K : G ∙ K ⟹ G' ∙ K) (comp_twosided_disp_functor FG HK) (comp_twosided_disp_functor FG' HK). Proof. simple refine (_ ,, _). - exact post_whisker_twosided_disp_nat_trans_data. - exact post_whisker_twosided_disp_nat_trans_laws. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor.