Synthetic topos theory
[0055] Definition

Let \(U\) be a universe, let \(C\) be a \(U\)-logos, let \(I\) be a partially ordered object in \(C\), and let \(n\) be a natural number. We define \(\Delta _{I}\lbrack n\rbrack \) to be the object in \(C\) that classifies (non-strictly) increasing sequences in \(I\) of length \(n\). When \(I\) has least and greatest elements, face maps and degeneracy maps between \(\Delta _{I}\lbrack n\rbrack \)'s can also be defined.