Theorem SSet.Truncated.HomotopyCategory.lift_unique'

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.Truncated.HomotopyCategory.lift_unique'View on Github →

2024-12-20 00:42

Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

feat(AlgebraicTopology/HomotopyCat): SSet.hoFunctor (#16783) …

Added SSet.Truncated.HomotopyCategory.lift_unique'View on Github →