proposition: Proposition isaprop_2cells_cat_to_bicat : isaprop_2cells cat_to_bicat.
proof: Proof. intros x y f g p q. apply homset_property. 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