proposition: Lemma isaprop_uo (c : C) : isaprop (D c).
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.catiso UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Univalence