Commit 2020-07-28 08:55 ce70305b
View on Github →feat(category_theory): monoidal_category (C ⥤ D) when D is monoidal (#3571)
When C
is any category, and D
is a monoidal category,
there is a natural "pointwise" monoidal structure on C ⥤ D
.
The initial intended application is tensor product of presheaves.