[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 $i:\mathord {\textnormal {\textsf {Level}}}$ . Then $\mathord {\textnormal {\textsf {Type}}}(i)$ is a judgment form.

[0020] Rule

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.

[0021] Rule

We work in the core type theory. Let $i_{1},i_{2}:\mathord {\textnormal {\textsf {Level}}}$ , let $A:\mathord {\textnormal {\textsf {Type}}}(i_{1})$ , and suppose that $i_{1}\le i_{2}$ . Then $A:\mathord {\textnormal {\textsf {Type}}}(i_{2})$ .

Note that universes that classify $\mathord {\textnormal {\textsf {Type}}}(i)$ '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.