Definition locally_iso_contractible_disp_iso {C : category} (D : disp_cat C) {x y : C} {f : z_iso x y} {xx : D x} {yy : D y} (ff : xx -->[ f ] yy) (HD : locally_iso_contractible D) (HD' : locally_propositional D) : is_z_iso_disp f ff. Proof. simple refine (_ ,, _ ,, _). - apply (HD y x (z_iso_inv f) yy xx). - apply HD'. - apply HD'. Defined.
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.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.