Definition disp_cat_is_locally_propositional {C : category} (D : disp_cat C) (HD : adds_structure D) : locally_propositional D. Proof. intros x y f xx yy. apply invproofirrelevance. intros ff gg. unfold faithful in HD. specialize (HD (x ,, xx) (y ,, yy) f). pose (proofirrelevance _ HD ((f ,, ff) ,, idpath _) ((f ,, gg) ,, idpath _)) as HD'. simpl in HD'. pose (maponpaths pr1 HD') as p. refine (_ @ fiber_paths p). refine (!_) ; cbn. apply transportf_set. apply homset_property. 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.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.