Definition enrichment_laws {C : precategory_data} {V : monoidal_cat} (E : enrichment_data C V) : UU := (∏ (x y : C), mon_lunitor (E ⦃ x , y ⦄) = enriched_id E y #⊗ identity _ · enriched_comp E x y y) × (∏ (x y : C), mon_runitor (E ⦃ x , y ⦄) = identity _ #⊗ enriched_id E x · enriched_comp E x x y) × (∏ (w x y z : C), enriched_comp E x y z #⊗ identity (E ⦃ w, x ⦄) · enriched_comp E w x z = mon_lassociator _ _ _ · identity _ #⊗ enriched_comp E w x y · enriched_comp E w y z) × (∏ (x y : C) (f : x --> y), enriched_to_arr E (enriched_from_arr E f) = f) × (∏ (x y : C) (f : I_{V} --> E ⦃ x , y ⦄), enriched_from_arr E (enriched_to_arr E f) = f) × (∏ (x : C), enriched_to_arr E (enriched_id E x) = identity x) × (∏ (x y z : C) (f : x --> y) (g : y --> z), f · g = enriched_to_arr E (mon_linvunitor I_{V} · (enriched_from_arr E g #⊗ enriched_from_arr E f) · enriched_comp E x y z)).
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.