Definition enriched_precomp : enriched_functor_category E₂ E₃ ⟶ enriched_functor_category E₁ E₃. Proof. use make_functor. - exact enriched_precomp_data. - exact is_functor_enriched_precomp. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory. Require Import UniMath.CategoryTheory.Monoidal.Categories.