proposition: Proposition is_univalent_2_0_cat_to_bicat (HC : is_univalent C) : is_univalent_2_0 cat_to_bicat.
proof: Proof. use discrete_bicat_univalent_2_0. - exact is_discrete_cat_to_bicat. - refine (transportf is_univalent _ HC). use category_eq. apply idpath. 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