fact: Definition pr2_dirprod_invertible_2cell {B : bicat} (D₁ D₂ : disp_bicat B) {x y : total_bicat (disp_dirprod_bicat D₁ D₂)} {f g : x --> y} (α : invertible_2cell f g) : @invertible_2cell (total_bicat D₂) (pr1 x ,, pr22 x) (pr1 y ,, pr22 y) (pr1 f ,, pr22 f) (pr1 g ,, pr22 g).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.Initial UniMath.Bicategories.Core.Examples.Final UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.Core.Univalence UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.DisplayedBicats.DispAdjunctions UniMath.Bicategories.DisplayedBicats.DispUnivalence