proposition: Proposition locally_groupoid_cat_to_bicat : locally_groupoid cat_to_bicat.
proof: Proof. intros x y f g α. refine (!α ,, _ ,, _). - apply isaprop_2cells_cat_to_bicat. - apply isaprop_2cells_cat_to_bicat. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Discreteness UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.AdjointUnique UniMath.Bicategories.Core.Univalence