proposition: Proposition idtoiso_twosided_disp_inv {C₁ C₂ : category} {D : twosided_disp_cat C₁ C₂} {x : C₁} {y : C₂} {xy xy' : D x y} (p : xy = xy') : pr1 (idtoiso_twosided_disp (idpath _) (idpath _) (!p)) = iso_inv_twosided_disp (idtoiso_twosided_disp (idpath _) (idpath _) p).
proof: Proof. induction p ; cbn. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness