A simplicial set is just a simplicial object in
Type-valued presheaf on the simplex category.
(One might be tempted to call these "simplicial types" when working in type-theoretic foundations, but this would be unnecessarily confusing given the existing notion of a simplicial type in homotopy type theory.)
We define the standard simplices
Δ[n] as simplicial sets,
and their boundaries
∂Δ[n] and horns
(The notations are available via
Future work #
There isn't yet a complete API for simplices, boundaries, and horns.
As an example, we should have a function that constructs
from a non-surjective order preserving function
Fin n → Fin n
Δ[n] ⟶ ∂Δ[n].