Synthetic topos theory
[002T] Notation

Let \(T_{1}\) be a base type theory, let \(T_{2}\) be a type theory internal to \(T_{1}\), and let \(T_{3}\) be a type theory internal to \(T_{2}\). We work in \(T_{1}\). Since the translation \(\mathord {\textnormal {\textsf {GS}}}_{T_{2}}:T_{2}\rightarrow \mathord {\textnormal {\textsf {Self}}}\) is a right adjoint, it preserves arbitrary algebraic structures. In particular, it takes \(T_{3}\) to a type theory internal to \(T_{1}\) which we refer to as \(\mathord {\textnormal {\textsf {Glob}}}_{T_{2}}(T_{3})\) and call the globalization of \(T_{3}\).