Def CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete

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