Simplicial homotopy theory

Stream: maths

[Saul Glasman]

Hi all,

I'm interested in beginning to formalize some elements of simplicial homotopy theory - two milestones I have in mind are the standard model structure on the category of simplicial sets and the Dold-Kan correspondence. Has anyone worked on this at all? (I know about the "sset" branch of mathlib, which is presumably where such an effort would start.)

[Scott Morrison]

I think sset is the most advanced in that direction! Go for it.