Theorem SSet.OneTruncation₂.id_edge

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.OneTruncation₂.id_edge View on Github →

2024-12-20 00:42

Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

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

Added SSet.OneTruncation₂.id_edge View on Github →