Let \(T\) be a base type theory. The type theory \(T\) itself is regarded as a type theory internal to \(T\) which we call the self-internalization of \(T\). Inside \(T\), the self-internalization of \(T\) is referred to as \(\mathord {\textnormal {\textsf {Self}}}\). More precisely, \(\mathord {\textnormal {\textsf {Self}}}\) is described as follows. We work in \(T\).

• -Let \(i:\mathord {\textnormal {\textsf {Level}}}\). Then \(\mathord {\textnormal {\textsf {Ctx}}}_{\mathord {\textnormal {\textsf {Self}}}}(i)\equiv \mathcal {U}(i)\).
• -Let \(i:\mathord {\textnormal {\textsf {Level}}}\) and let \(\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{\mathord {\textnormal {\textsf {Self}}}}(i)\). Then \(\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Self}}}}(\Gamma \vdash \mathord {\textnormal {\textsf {Type}}}(i))\equiv \Gamma \rightarrow \mathcal {U}(i)\).
• -Let \(i:\mathord {\textnormal {\textsf {Level}}}\), let \(\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{\mathord {\textnormal {\textsf {Self}}}}(i)\), and let \(A:\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Self}}}}(\Gamma \vdash \mathord {\textnormal {\textsf {Type}}}(i))\). Then \(\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Self}}}}(\Gamma \vdash A)\equiv (x:\Gamma )\rightarrow A(x)\).