## Stream: maths

### Topic: Simplicial homotopy theory

#### Saul Glasman (Oct 20 2020 at 22:59):

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 (Oct 20 2020 at 23:01):

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

Last updated: May 14 2021 at 19:21 UTC