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