[002P] -- Synthetic topos theory

[002P] Definition

Let $T_{1}$ be a base type theory and let $T_{2}$ be a type theory internal to $T_{1}$ . We work in $T_{1}$ . We define a translation

\mathord {\textnormal {\textsf {GS}}}_{T_{2}}:T_{2}\rightarrow \mathord {\textnormal {\textsf {Self}}}

called the global section translation as follows.

-Let $i:\mathord {\textnormal {\textsf {Level}}}$ and let $\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i)$ . Then $\mathord {\textnormal {\textsf {GS}}}_{T_{2}}(\Gamma )\equiv \mathord {\textnormal {\textsf {Hom}}}_{\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i)}(\epsilon ,\Gamma )$ .
-Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i)$ , and let $A:\mathord {\textnormal {\textsf {D}}}_{T_{2}}(\Gamma \vdash \mathord {\textnormal {\textsf {Type}}}(i))$ . Then $\mathord {\textnormal {\textsf {GS}}}_{T_{2}}(A)\equiv x\mapsto \mathord {\textnormal {\textsf {D}}}_{T_{2}}({}\vdash A(x))$ .
-Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i)$ , let $A:\mathord {\textnormal {\textsf {D}}}_{T_{2}}(\Gamma \vdash \mathord {\textnormal {\textsf {Type}}}(i))$ , and let $a:\mathord {\textnormal {\textsf {D}}}_{T_{2}}(\Gamma \vdash A)$ . Then $\mathord {\textnormal {\textsf {GS}}}_{T_{2}}(a)\equiv x\mapsto a(x)$ .