Commit 2021-03-20 10:08 695d7f4f
View on Github →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.