Definition locally_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_contractible D) : is_z_iso_disp f ff. Proof. simple refine (_ ,, _ ,, _). - apply HD. - apply (locally_propositional_if_locally_contractible _ HD). - apply (locally_propositional_if_locally_contractible _ 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.