Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Let \(n:\mathord {\textnormal {\textsf {Nat}}}\). We define \(\Delta \lbrack n\rbrack :\mathcal {T}\) to be the type of (non-strictly) increasing sequences in \(\mathbb {I}\) of length \(n\). Face maps and degeneracy maps between \(\Delta \lbrack n\rbrack \)'s can also be defined.