Definition disp_hom_disp_z_iso_weq_invertible_2cell {B : bicat} {D : disp_bicat B} {x y : B} {f g : x --> y} {α : f ==> g} {Hα : is_invertible_2cell α} {xx : D x} {yy : D y} {ff : disp_hom xx yy f} {gg : disp_hom xx yy g} (αα : ff -->[ α ] gg) : (@is_z_iso_disp _ (disp_hom xx yy) _ _ (α ,, is_inv2cell_to_is_z_iso _ Hα) _ _ αα) ≃ is_disp_invertible_2cell Hα αα.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Invertible_2cells.