fact: Definition make_two_cat_category (C : two_cat_data) (HC₁ : is_precategory C) (HC₂ : has_homsets C) : two_cat_category := C ,, HC₁ ,, HC₂.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence