A.2.1 Contexts

A context is a list

 $x_{1}\mathord{:}A_{1},x_{2}\mathord{:}A_{2},\ldots,x_{n}\mathord{:}A_{n}$

which indicates that the distinct variables $x_{1},\ldots,x_{n}$ are assumed to have types $A_{1},\ldots,A_{n}$, respectively. The list may be empty. We abbreviate contexts with the letters $\Gamma$ and $\Delta$, and we may juxtapose them to form larger contexts.

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

Title A.2.1 Contexts
\metatable