Definition locally_contractible_to_obj_prop {C : category} (D : disp_cat C) (HD₁ : is_univalent_disp D) (HD₂ : locally_contractible D) : ∏ (x : C), isaprop (D x). Proof. intros x xx yy. specialize (HD₁ x x (idpath _) xx yy). apply (isofhlevelweqb 0 (make_weq _ HD₁)). use isofhleveltotal2. - apply HD₂. - intro f. apply iscontraprop1. + apply isaprop_is_z_iso_disp. + apply locally_contractible_disp_iso. apply HD₂. 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.