Definition locally_iso_contractible_to_obj_prop {C : category} (D : disp_cat C) (HD₁ : is_univalent_disp D) (HD₂ : locally_iso_contractible D) (HD₃ : locally_propositional 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_iso_contractible_disp_iso. * apply HD₂. * exact 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.