fact: Definition two_cat_cells (C : two_cat_data) {a b : C} (f g : C⟦a, b⟧) : UU := pr12 C a b f g.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence