Lemma z_iso_disp_iscontr {c : C} (d1 d2 : D c) : iscontr (z_iso_disp (idtoiso (idpath c)) d1 d2). 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.
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.