Commit 2024-12-20 15:29 92c2d0cb

feat(CategoryTheory/Enriched): functoriality of the enrichment of functor categories (#18414) Let C be a V-enriched ordinary category. Functor categories J ⥤ C have been V-enriched in #18009. Given two functors F₁ and F₂ in J ⥤ C, we use the previous results for functors Under j ⥤ C for all j : J in order to construct functorEnrichedHom V F₁ F₂ : J ⥤ V, and show that the limit of this functor identifies to enrichedHom V F₁ F₂.