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. apply isapropdirprod; apply homsets_disp. Qed.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core.