proposition: Lemma isaprop_is_disp_inverse {C : category} {D : disp_cat C} {x y : C} (f : x --> y) (g: y --> x) (isinv: is_inverse_in_precat f g) {xx : D x} {yy : D y} (ff : xx -->[f] yy) (gg : yy -->[g] xx) : isaprop (is_disp_inverse isinv ff gg).
proof: Proof. apply isapropdirprod; apply homsets_disp. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core