Let \(T_{1}\) be a type theory and let \(T_{2}\) be a type theory internal to \(T_{1}\). We work in \(T_{1}\).

• -Let \(i:\mathord {\textnormal {\textsf {Level}}}\). Then \(\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i):\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))\) denotes the type of contexts of level \(i\) in \(T_{2}\). It also denotes the category of contexts of level \(i\) and morphisms between them.
• -Let \(i:\mathord {\textnormal {\textsf {Level}}}\) and let \(\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i)\). Then \(\mathord {\textnormal {\textsf {D}}}_{T_{2}}(\Gamma \vdash \mathord {\textnormal {\textsf {Type}}}(i)):\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))\) denotes the type of types of level \(i\) in context \(\Gamma \) in \(T_{2}\).
• -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 {D}}}_{T_{2}}(\Gamma \vdash A):\mathord {\textnormal {\textsf {Type}}}(i)\) denotes the type of elements of \(A\) in context \(\Gamma \) in \(T_{2}\).