Definition two_cat_data : UU := ∑ (C : precategory_data) (cells_C : ∏ (x y : C), x --> y → x --> y → UU), (∏ (x y : C) (f : x --> y), cells_C _ _ f f) × (∏ (x y : C) (f g h : x --> y), cells_C _ _ f g → cells_C _ _ g h → cells_C _ _ f h) × (∏ (x y z : C) (f : x --> y) (g1 g2 : y --> z), cells_C _ _ g1 g2 → cells_C _ _ (f · g1) (f · g2)) × (∏ (x y z : C) (f1 f2 : x --> y) (g : y --> z), cells_C _ _ f1 f2 → cells_C _ _ (f1 · g) (f2 · g)).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Univalence.