proposition: Lemma z_iso_disp_iscontr {c : C} (d1 d2 : D c) : iscontr (z_iso_disp (idtoiso (idpath c)) d1 d2).
proof: Proof. use tpair. - refine (_ ,, _). apply only_isos_above_an_id. - intro i. use subtypePath. { intro ; apply isaprop_is_z_iso_disp. } apply proofirrelevance. apply isapropifcontr. apply uf. 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