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.