Let \(T\) be a base type theory. We work in \(T\). Let \(n:\mathord {\textnormal {\textsf {Nat}}}\). We define the standard \(n\)-simplex \(\Delta \lbrack n\rbrack :\mathcal {S}(\mathord {\textnormal {\textsf {LO}}},0)\) to be \(\mathord {\textnormal {\textsf {e}}}_{{\langle n\rangle }_{\mathord {\textnormal {\textsf {LO}}}}}\).