Def CategoryTheory.Cat.fromChosenTerminalEquiv

Modification history

2025-07-12 12:51
Mathlib/CategoryTheory/Monoidal/Cartesian/Cat.lean
feat(Bicategory/CatEnriched): 2-cat from Cat-enriched cat (#25784) …
Added CategoryTheory.Cat.fromChosenTerminalEquivView on Github →