Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos. We define a translation \(Z\mapsto {\mathopen {[\negthinspace [}Z\mathclose {]\negthinspace ]}}^{X}\) from \(\mathord {\textnormal {\textsf {Sp}}}\) to \(\mathord {\textnormal {\textsf {Sh}}}(X)\) by \({\mathopen {[\negthinspace [}Z\mathclose {]\negthinspace ]}}^{X}\equiv \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}({X}^{*}(Z))\).