Let \(T_{1}\) be a type theory and let \(T_{2}\) be a type theory internal to \(T_{1}\). We work in \(T_{1}\). When we mention an object in \(T_{2}\), the object is understood in the empty context in \(T_{2}\). For example, “let \(A:\mathord {\textnormal {\textsf {Type}}}(i)\) in \(T_{2}\)” means “let \(A:\mathord {\textnormal {\textsf {D}}}_{T_{2}}({}\vdash \mathord {\textnormal {\textsf {Type}}}(i))\)”.