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.