Def CategoryTheory.Cat.isoDiscretePUnitOfIsTerminal

Modification history

2025-07-22 07:13
Mathlib/CategoryTheory/Category/Cat/Terminal.lean
Feat(CategoryTheory): terminal categories with an application to hoFunctor (#25781) …
Added CategoryTheory.Cat.isoDiscretePUnitOfIsTerminalView on Github →