# A closed monoidal category is enriched in itself #

From the data of a closed monoidal category `C`

, we define a `C`

-category structure for `C`

.
where the hom-object is given by the internal hom (coming from the closed structure).

We use `scoped instance`

to avoid potential issues where `C`

may also have
a `C`

-category structure coming from another source (e.g. the type of simplicial sets
`SSet.{v}`

has an instance of `EnrichedCategory SSet.{v}`

as a category of simplicial objects;
see `AlgebraicTopology/SimplicialCategory/SimplicialObject`

).

All structure field values are defined in `Closed/Monoidal`

.

def
CategoryTheory.MonoidalClosed.instEnrichedCategory
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalClosed C]
:

For `C`

closed monoidal, build an instance of `C`

as a `C`

-category

## Equations

- One or more equations did not get rendered due to their size.