what belongs in the SimplicialSet folder on mathlib?

Stream: mathlib4

[Emily Riehl]

In PR #16782, @Joël Riou is suggesting moving AlgebraicTopology/SimplicialSet.lean to AlgebraicTopology/SimplicialSet/Basic.lean. This makes a lot of sense to me, but I'm wondering what else in the AlgebraicTopology folder might belong in the SimplicialSet subfolder.

[Emily Riehl]

Arguably, KanComplex, Nerve, and QuasiCategory all belong there. The other free floating files in this directory are either prerequisites (eg SimplexCategory) or deal with the more general simplicial objects.

[Emily Riehl]

I'm wondering what @Johan Commelin thinks in particular. Also tagging @Mario Carneiro

[Johan Commelin]

Yeah, please move those other files as well