Definition rel_disp_cat_id_comp : twosided_disp_cat_id_comp rel_disp_cat_ob_mor. Proof. simple refine (_ ,, _). - exact (λ X Y R x y r, r). - exact (λ X₁ X₂ X₃ Y₁ Y₂ Y₃ R₁ R₂ R₃ f₁ f₂ g₁ g₂ α β x y r, β _ _ (α _ _ r)). 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.