Definition disp_hom_disp_z_iso_to_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) (Hαα : @is_z_iso_disp _ (disp_hom xx yy) _ _ (α ,, is_inv2cell_to_is_z_iso _ Hα) _ _ αα) : is_disp_invertible_2cell Hα αα. Proof. simple refine (_ ,, (_ ,, _)). - exact (inv_mor_disp_from_z_iso Hαα). - abstract (cbn; etrans; [apply (inv_mor_after_z_iso_disp Hαα)|]; unfold transportb; apply maponpaths_2 ; apply cellset_property). - abstract (cbn; etrans; [ apply (z_iso_disp_after_inv_mor Hαα) |]; 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.