Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos.

• -\(\mathord {\textnormal {\textsf {w}}}_{X}:\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Glob}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathord {\textnormal {\textsf {Sp}}})}({}\vdash {X}^{*}(X))\).
• -The translation \(\mathord {\textnormal {\textsf {Sp}}}/(x:X)\rightarrow \mathord {\textnormal {\textsf {Glob}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathord {\textnormal {\textsf {Sp}}})\) defined by \(Z\mapsto ({X}^{*}(Z))[x\mathrel {:\equiv }\mathord {\textnormal {\textsf {w}}}_{X}]\) is an equivalence.