Definition locally_propositional_to_obj_set {C : category} (D : disp_cat C) (HD₁ : is_univalent_disp D) (HD₂ : locally_propositional D) : ∏ (x : C), isaset (D x). Proof. intros x xx yy. specialize (HD₁ x x (idpath _) xx yy). apply (isofhlevelweqb 1 (make_weq _ HD₁)). use isofhleveltotal2. - apply HD₂. - intro. apply isaprop_is_z_iso_disp. 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.