mathlib

695d7f4f - refactor(algebraic_topology/simplex_category): Make simplex_category universe polymorphic. (#6761)

refactor(algebraic_topology/simplex_category): Make simplex_category universe polymorphic. (#6761) This PR changes the definition of `simplex_category` so that it becomes universe polymorphic. This is useful when we want to take (co)limits of simplicial objects indexed by categories constructed out of `simplex_category`. This PR also makes a small wrapper around morphisms in `simplex_category` for hygiene purposes, and introduces a notation `X _[n]` for the n-th term of a simplicial object X. Note: this PR makes `simplex_category` and `simplex_category.hom` irreducible. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>