Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos. By [002W], we have a translation

\(\mathord {\textnormal {\textsf {Sp}}}\rightarrow \mathord {\textnormal {\textsf {Glob}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathord {\textnormal {\textsf {Sp}}})\) that preserves all the structures of the type theory of spaces. We refer to this translation as \(Z\mapsto {X}^{*}(Z)\).