Definition enrichment_data (C : precategory_data) (V : monoidal_cat) : UU := ∑ (arr : C → C → V), (∏ (x : C), I_{V} --> arr x x) × (∏ (x y z : C), arr y z ⊗ arr x y --> arr x z) × (∏ (x y : C), x --> y → I_{V} --> arr x y) × (∏ (x y : C), I_{V} --> arr x y → x --> y).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import MonoidalNotations.