Def CategoryTheory.CatEnrichedOrdinary.toBase

Modification history

2025-07-12 12:51

Mathlib/CategoryTheory/Bicategory/CatEnriched.lean

feat(Bicategory/CatEnriched): 2-cat from Cat-enriched cat (#25784) …

Added CategoryTheory.CatEnrichedOrdinary.toBase View on Github →