warning: new PR will move some simplicial sets files

Stream: Infinity-Cosmos

[Emily Riehl]

Just a heads up to folks who might be impacted: there's a new PR #17620 (by request) that will move four files:

• SimplicialSet.lean
• Nerve.lean
• Quasicategory.lean
• KanComplex.lean
  into the SimplicialSet subfolder and rename the former to Basic.

Feel free to comment on there now. I'll post again here when/if the change is merged.

[Emily Riehl]

Merged!