# Commit 2020-08-02 11:46 52c0b421

View on Github →feat(category_theory): Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D (#3576)
When `D`

is a monoidal category,
monoid objects in `C ⥤ D`

are the same thing as functors from `C`

into the monoid objects of `D`

.
This is formalised as:

`Mon_functor_category_equivalence : Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D`

The intended application is that as`Ring ≌ Mon_ Ab`

(not yet constructed!), we have`presheaf Ring X ≌ presheaf (Mon_ Ab) X ≌ Mon_ (presheaf Ab X)`

, and we can model a module over a presheaf of rings as a module object in`presheaf Ab X`

.