Definition mortoid_discrete_twosided_disp {C₁ C₂ : category} {D : twosided_disp_cat C₁ C₂} (HD : discrete_twosided_disp_cat D) {x : C₁} {y : C₂} (xy₁ xy₂ : D x y) (r : xy₁ -->[ identity x ][ identity y ] xy₂) : xy₁ = xy₂. Proof. use (isotoid_twosided_disp (pr22 HD) (idpath _) (idpath _)). simple refine (r ,, _). apply HD. 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.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.