Let \(T\) be a type theory. Inside \(T\), the type theory of spaces in \(T\) is referred to as \(\mathord {\textnormal {\textsf {Sp}}}\).