proposition: Proposition is_discrete_cat_to_bicat : is_discrete_bicat cat_to_bicat.
proof: Proof. repeat split. - exact is_univalent_2_1_cat_to_bicat. - exact locally_groupoid_cat_to_bicat. - exact isaprop_2cells_cat_to_bicat. Qed.
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