Theorem SSet.OneTruncation₂.id_edge

Modification history

2026-05-17 20:27
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
chore: remove declarations deprecated between 2021-05-15 and 2025-11-15 (#39405) …
Deleted SSet.OneTruncation₂.id_edgeView on Github →
2025-12-05 11:03
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
refactor(AlgebraicTopology): refactor the homotopy category and the nerve adjunction (#31174) …
Modified SSet.OneTruncation₂.id_edgeView on Github →
2024-12-20 00:42
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
feat(AlgebraicTopology/HomotopyCat): SSet.hoFunctor (#16783) …
Added SSet.OneTruncation₂.id_edgeView on Github →