Definition enriched_precomp_data : functor_data (enriched_functor_category E₂ E₃) (enriched_functor_category E₁ E₃). Proof. use make_functor_data. - exact (λ G, F ∙ _ ,, functor_comp_enrichment EF (pr2 G)). - exact (λ _ _ τ, pre_whisker F (pr1 τ) ,, pre_whisker_enrichment EF (pr2 τ)). 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.