Definition pre_whisker_enriched_functor_category {V : monoidal_cat} {C₁ C₂ C₃ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} {E₃ : enrichment C₃ V} (F : enriched_functor_category E₁ E₂) {G₁ G₂ : enriched_functor_category E₂ E₃} (τ : G₁ --> G₂) : comp_enriched_functor_category F G₁ --> comp_enriched_functor_category F G₂. Proof. simple refine (_ ,, _). - exact (pre_whisker (pr11 F) (pr1 τ)). - use pre_whisker_enrichment. exact (pr2 τ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.FunctorCategory. 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.HomFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Import MonoidalNotations. Section EnrichmentFromArr. End EnrichmentFromArr.