Commit 2025-02-06 01:05 7e090dcb
View on Github →feat(CategoryTheory): a closed monoidal category is an ordinary enriched category over itself (#21436)
Let C
be a closed monoidal category. It was previously shown (#17326) that C
is enriched over itself. In this PR, we show that the category structure on C
is determined by this enriched category structure, i.e. EnrichedOrdinaryCategory C C
holds.