Commit 2025-02-04 06:23 7e37e861
View on Github →feat(CategoryTheory/Enriched): enrichement of functor categories over a functor category (#18976)
Let C be a category that is enriched over a monoidal category V in such a way that the category structure and the enriched category structure are compatible. If J is a category and that V has certain limits, then the functor category J ⥤ C is enriched over J ⥤ V.