proposition: Proposition is_univalent_univalent_two_cat (C : univalent_two_cat) : is_univalent (category_from_two_cat_data C).
proof: Proof. exact (pr2 C). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence