Topic: Simplicial homotopy theory
Saul Glasman (Oct 20 2020 at 22:59):
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 (Oct 20 2020 at 23:01):
sset is the most advanced in that direction! Go for it.
Last updated: May 14 2021 at 19:21 UTC