Proposition idtoiso_twosided_disp_identity {C₁ C₂ : category} {D : strict_twosided_disp_cat C₁ C₂} {x : C₁} {y : C₂} {xy : D x y} (p : xy = xy) : pr1 (idtoiso_twosided_disp (idpath _) (idpath _) p) = id_two_disp xy. Proof. assert (p = idpath _) as s. { apply is_strict_strict_twosided_disp_cat. } rewrite s. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness.