Commit 2021-03-20 10:08 695d7f4f

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.