Synthetic topos theory

[001Y] Core type theory

We will introduce several type theories. The core type theory is the basis for all of those type theories.

[001Z] Rule

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

[0020] Rule

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

[0021] Rule

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

Note that universes that classify Type(i)\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.