We work in the core type theory. Let . Then is a judgment form.
[001Y] Core type theory
We will introduce several type theories. The core type theory is the basis for all of those type theories.
We work in the core type theory. Let and let . Then is a judgment form.
We work in the core type theory. Let , let , and suppose that . Then .
Note that universes that classify 's are not introduced at this moment.
By a type theory we mean an extension of the core type theory by rules that construct types, elements, and definitional equality.