Definition disp_hom_disp_invertible_2cell_to_z_iso {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) (Hαα : is_disp_invertible_2cell Hα αα) : @is_z_iso_disp _ (disp_hom xx yy) _ _ (α ,, is_inv2cell_to_is_z_iso _ Hα) _ _ αα. Proof. pose (d := (αα ,, Hαα) : disp_invertible_2cell (α ,, Hα) ff gg). simple refine (_ ,, (_ ,, _)). - exact (disp_inv_cell d). - abstract (cbn; unfold transportb; etrans; [ exact (disp_vcomp_linv d) |]; unfold transportb; apply maponpaths_2; apply cellset_property). - abstract (cbn; unfold transportb; etrans; [ exact (disp_vcomp_rinv d) |]; unfold transportb; apply maponpaths_2; apply cellset_property). Defined.
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.