Definition eq_twosided_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_data F G D D'} {FG' : twosided_disp_functor_data F' G' D D'} {τθ τθ' : twosided_disp_nat_trans τ θ FG FG'} (p : ∏ (x : C₁) (y : C₂) (xy : D x y), τθ x y xy = τθ' x y xy) : τθ = τθ'.
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.