fact: Definition is_disp_invertible_2cell_twosided_disp_cat_help {C₁ C₂ : bicat_of_univ_cats} {F G : C₁ --> C₂} (τ : invertible_2cell F G) (Hτ := is_invertible_2cell_to_is_nat_z_iso _ (pr2 τ)) {D₁ : disp_bicat_twosided_disp_cat C₁} {D₂ : disp_bicat_twosided_disp_cat C₂} {FF : D₁ -->[ F ] D₂} {GG : D₁ -->[ G ] D₂} (ττ : FF ==>[ τ ] GG) (Hττ : ∏ (x y : pr1 C₁) (f : pr1 D₁ x y), is_iso_twosided_disp (Hτ x) (Hτ y) (pr1 ττ x y f)) : is_disp_invertible_2cell (is_nat_z_iso_to_is_invertible_2cell _ Hτ) ττ.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All 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.PrecategoryBinProduct UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfDispCats UniMath.Bicategories.DisplayedBicats.UnivalenceTechniques UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.CatDiag UniMath.Bicategories.DisplayedBicats.DispPseudofunctor