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'). Proof. use weq_iso. - exact twosided_disp_nat_trans_to_disp_nat_trans. - exact twosided_disp_nat_trans_from_disp_nat_trans. - abstract (intros τθ ; use subtypePath ; [ intro ; apply isaprop_twosided_disp_nat_trans_laws | ] ; apply idpath). - abstract (intros τθ ; use subtypePath ; [ intro ; apply isaprop_disp_nat_trans_axioms | ] ; apply idpath). 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.