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 Mathlib/AlgebraicTopology/SimplicialCategory/SimplicialObject.lean).
All structure field values are defined in Mathlib/CategoryTheory/Closed/Monoidal.lean.
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.