fact: Definition twosided_disp_nat_trans_weq_disp_nat_trans {C₁ C₁' C₂ C₂' : category} {F F' : C₁ ⟶ C₁'} (τ : F ⟹ F') {G G' : C₂ ⟶ C₂'} (θ : G ⟹ G') {D : twosided_disp_cat C₁ C₂} {D' : twosided_disp_cat C₁' C₂'} (FG : twosided_disp_functor F G D D') (FG' : twosided_disp_functor F' G' D D') : twosided_disp_nat_trans τ θ FG FG' ≃ disp_nat_trans (pair_nat_trans τ θ) (two_sided_disp_functor_to_disp_functor FG) (two_sided_disp_functor_to_disp_functor FG').
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete UniMath.CategoryTheory.TwoSidedDisplayedCats.Total UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor