Commit 2021-02-26 10:06 dd5363b5

feat(algebraic_topology): introduce the simplex category (#6173)

• introduce simplex_category, with objects nat and morphisms n ⟶ m order-preserving maps from fin (n+1) to fin (m+1).
• prove the simplicial identities
• show the category is equivalent to NonemptyFinLinOrd This is the start of simplicial sets, moving and completing some of the material from @jcommelin's sset branch. Dold-Kan is the obvious objective; apparently we're going to need it for lean-liquid at some point. The proofs of the simplicial identities are bad and slow. They involve extravagant use of nonterminal simp (simp? doesn't seem to give good answers) and lots of linarith bashing. Help welcome, especially if you love playing with inequalities in nat involving lots of -1s.