Definition is_functor_enrichment {V : monoidal_cat} {C₁ C₂ : category} {F : C₁ ⟶ C₂} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} (FE : functor_enrichment_data F E₁ E₂) : UU := (∏ (x : C₁), enriched_id E₁ x · FE x x = enriched_id E₂ (F x)) × (∏ (x y z : C₁), enriched_comp E₁ x y z · FE x z = FE y z #⊗ FE x y · enriched_comp E₂ (F x) (F y) (F z)) × (∏ (x y : C₁) (f : x --> y), enriched_from_arr E₂ (#F f) = enriched_from_arr E₁ f · FE x y).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.Limits.Terminal. Import MonoidalNotations.