Def CategoryTheory.CatEnrichedOrdinary.hComp

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.hComp View on Github →