Lemma only_isos_above_an_iso {c1 c2 : C} {f : C⟦c1,c2⟧} {d1 : D c1} {d2 : D c2} (ff : d1 -->[f] d2) : ∏ fi : is_z_isomorphism f, is_z_iso_disp (_ ,, fi) ff. Proof. intro fi. use tpair. * apply (uf c2 c1 (pr1 fi)). * split ; (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.