Lemma isaprop_uo (c : C) : isaprop (D c). Proof. intros d1 d2. use tpair. - use (isotoid_disp Duniv (idpath c)). exact (_ ,, only_isos_above_an_id d1 d2). - intro. apply proofirrelevance. apply isapropifcontr. refine (iscontrweqb _ (z_iso_disp_iscontr d1 d2)). unfold is_univalent_disp in Duniv. refine ( _ ,, _). apply Duniv. Qed.
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.catiso. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.