We work in the core type theory. Let \(i:\mathord {\textnormal {\textsf {Level}}}\). Then \(\mathord {\textnormal {\textsf {Type}}}(i)\) is a judgment form.