Definition set_rel_disp_cat_ob_mor : twosided_disp_cat_ob_mor SET SET. Proof. simple refine (_ ,, _). - exact (λ (X : hSet) (Y : hSet), X → Y → hSet). - exact (λ (X₁ : hSet) X₂ (Y₁ : hSet) Y₂ R₁ R₂ f g, ∏ (x : X₁) (y : Y₁), R₁ x y → R₂ (f x) (g y)). 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.Isos. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedFibration.