A.2.1 Contexts

A context is a list

$$x_1\mathrm{:}{A}_1,x_2\mathrm{:}{A}_2,\mathrm{\dots },x_n\mathrm{:}{A}_n$$

which indicates that the distinct variables $x_1,\mathrm{\dots },x_n$ are assumed to have types $A_1,\mathrm{\dots },A_n$, respectively. The list may be empty. We abbreviate contexts with the letters $\mathrm{\Gamma }$ and $\mathrm{\Delta }$, and we may juxtapose them to form larger contexts.

The judgment $\mathrm{\Gamma }\mathrm{𝖼𝗍𝗑}$ formally expresses the fact that $\mathrm{\Gamma }$ is a well-formed context, and is governed by the rules of inference *[right=$\mathrm{𝖼𝗍𝗑}$-emp]   $\cdot$ $\mathrm{𝖼𝗍𝗑}$ *[right=$\mathrm{𝖼𝗍𝗑}$-ext] x_1 : A_1, …, x_n-1 : A_n-1 ⊢A_n : $𝒰$ _i (x_1 : A_1, …, x_n : A_n) $\mathrm{𝖼𝗍𝗑}$ with a side condition for the second rule: the variable $x_n$ must be distinct from the variables $x_1,\mathrm{\dots },x_{n-1}$. Note that the hypothesis and conclusion of $\mathrm{𝖼𝗍𝗑}$-ext are judgments of different forms: the hypothesis says that in the context of variables $x_1,\mathrm{\dots },x_{n-1}$, the expression $A_n$ has type ${𝒰}_i$; while the conclusion says that the extended context $(x_1\mathrm{:}{A}_1,\mathrm{\dots },x_n\mathrm{:}{A}_n)$ is well-formed. (It is a meta-theoretic property of the system that if $x_1\mathrm{:}{A}_1,\mathrm{\dots },x_n\mathrm{:}{A}_n⊢b:B$ is derivable, then the context $(x_1\mathrm{:}{A}_1,\mathrm{\dots },x_n\mathrm{:}{A}_n)$ must be well-formed; thus $\mathrm{𝖼𝗍𝗑}$-ext does not need to hypothesize well-formedness of the context to the left of $x_n$.)

Title	A.2.1 Contexts