Def CategoryTheory.TransportEnrichment.enrichedOrdinaryCategory

Modification history

2025-11-23 17:11
Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
feat(Algebraic Topology): the strict bicategory of quasicategories (#31101) …
Added CategoryTheory.TransportEnrichment.enrichedOrdinaryCategoryView on Github →