Def SSet.isTerminalHoFunctorDeltaZero

Modification history

2025-12-05 11:03
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
refactor(AlgebraicTopology): refactor the homotopy category and the nerve adjunction (#31174) …
Modified SSet.isTerminalHoFunctorDeltaZeroView on Github →
2025-07-22 07:13
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
Feat(CategoryTheory): terminal categories with an application to hoFunctor (#25781) …
Added SSet.isTerminalHoFunctorDeltaZeroView on Github →