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.

Estimated changes