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}}}\) and let \(A:\mathord {\textnormal {\textsf {D}}}_{T_{2}}({}\vdash \mathord {\textnormal {\textsf {Type}}}(i))\). Then \(T_{2}/(x:A)\) denotes the slice type theory over \(A\). More precisely, it is described as follows.

• -Let \(j:\mathord {\textnormal {\textsf {Level}}}\). Then \(\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}/(x:A)}(j)\) is the full subcategory of \(\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(j)/(x:A)\) spanned by the display maps over \(x:A\) of level \(j\).
• -The types of types and elements are created by the domain projection \(\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}/(x:A)}(j)\rightarrow \mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(\_)\).