fact: Definition make_two_cat (C : two_precat) (HC : isaset_cells C) : two_cat := C ,, HC.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence