Commit 2025-01-24 10:30 f088ec9d
View on Github →chore(AlgebraicTopology): make stdSimplex a cosimplicial object (#20954)
The functor stdSimplex : SimplexCategory ⥤ SSet.{u} is redefined to the defeq type of cosimplicial objects in SSet. This allows the use of the notation stdSimplex.δ i instead of stdSimplex.map (SimplexCategory.δ i).