Definition twosided_disp_cat_ob_mor (C₁ C₂ : precategory_ob_mor) : UU := ∑ (D : C₁ → C₂ → UU), ∏ (x₁ x₂ : C₁) (y₁ y₂ : C₂), D x₁ y₁ → D x₂ y₂ → x₁ --> x₂ → y₁ --> y₂ → UU.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.