Definition make_two_cat_data (C : precategory_data) (cellsC : ∏ (x y : C), x --> y → x --> y → UU) (id : ∏ (x y : C) (f : x --> y), cellsC _ _ f f) (vC : ∏ (x y : C) (f g h : x --> y), cellsC _ _ f g → cellsC _ _ g h → cellsC _ _ f h) (lW : ∏ (x y z : C) (f : x --> y) (g1 g2 : y --> z), cellsC _ _ g1 g2 → cellsC _ _ (f · g1) (f · g2)) (rW : ∏ (x y z : C) (f1 f2 : x --> y) (g : y --> z), cellsC _ _ f1 f2 → cellsC _ _ (f1 · g) (f2 · g)) : two_cat_data := C ,, cellsC ,, id ,, vC ,, lW ,, rW.
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.