fact: Definition disp_bicat_of_opcleaving_disp_invertible_2cell_pointwise_inv {C C' : bicat_of_univ_cats} {F G : C --> C'} {α : F ==> G} (Hα : is_invertible_2cell α) {D : disp_bicat_of_opcleaving C} {D' : disp_bicat_of_opcleaving C'} {FF : D -->[ F ] D'} {GG : D -->[ G ] D'} (αα : FF ==>[ α ] GG) (Hαα : is_disp_invertible_2cell Hα αα) {x : (C : univalent_category)} (xx : (pr1 D : disp_univalent_category _) x) : is_z_iso_disp (make_z_iso' (pr1 α x) (is_invertible_2cell_to_is_nat_z_iso _ Hα x)) (pr11 αα x xx).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Adjunctions UniMath.CategoryTheory.DisplayedCats.Equivalences UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq UniMath.CategoryTheory.DisplayedCats.EquivalenceOverId UniMath.CategoryTheory.DisplayedCats.DisplayedCatEq UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispAdjunctions UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DisplayedBicats.Examples.FullSub UniMath.Bicategories.DisplayedBicats.Examples.Sigma UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat