proposition: Proposition is_univalent_2_1_cat_to_bicat : is_univalent_2_1 cat_to_bicat.
proof: Proof. intros x y f g. use isweqimplimpl. - exact (λ p, pr1 p). - apply homset_property. - use isaproptotal2. + intro. apply isaprop_is_invertible_2cell. + intros. 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