fact: Definition disp_locally_groupoid_over_id {B : bicat} (D : disp_bicat B) : UU := ∏ (a b : B) (f : B ⟦ a, b ⟧) (aa : D a) (bb : D b) (ff gg : aa -->[ f] bb) (xx : disp_2cells (id2_invertible_2cell f) ff gg), is_disp_invertible_2cell (is_invertible_2cell_id₂ f) xx.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Univalence