Definition twosided_disp_nat_trans_from_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'} (τθ : disp_nat_trans (pair_nat_trans τ θ) (two_sided_disp_functor_to_disp_functor FG) (two_sided_disp_functor_to_disp_functor FG')) : twosided_disp_nat_trans τ θ FG FG'. Proof. refine ((λ x y xy, τθ (x ,, y) xy) ,, _). abstract (intros x₁ x₂ y₁ y₂ f g xy₁ xy₂ fg ; cbn ; pose (@disp_nat_trans_ax _ _ _ _ _ _ _ _ _ τθ (x₁ ,, y₁) (x₂ ,, y₂) (f ,, g) xy₁ xy₂ fg) as p ; cbn in p ; rewrite p ; unfold transportb_disp_mor2, transportf_disp_mor2 ; rewrite twosided_prod_transport ; unfold transportb ; apply maponpaths_2 ; apply isasetdirprod ; apply homset_property). 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.