# 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{\U0001d5bc\U0001d5cd\U0001d5d1}$ formally expresses the fact that $\mathrm{\Gamma}$ is a well-formed context, and is governed by the rules of inference^{}
{mathpar}
\inferrule*[right=$\mathrm{\U0001d5bc\U0001d5cd\U0001d5d1}$-emp]
$\cdot $ $\mathrm{\U0001d5bc\U0001d5cd\U0001d5d1}$
\inferrule*[right=$\mathrm{\U0001d5bc\U0001d5cd\U0001d5d1}$-ext]
x_1 : A_1, …, x_n-1 : A_n-1 ⊢A_n : $\mathcal{U}$ _i
(x_1 : A_1, …, x_n : A_n) $\mathrm{\U0001d5bc\U0001d5cd\U0001d5d1}$
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{\U0001d5bc\U0001d5cd\U0001d5d1}$-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 ${\mathcal{U}}_{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}\u22a2b:B$ is derivable^{}, then the context $({x}_{1}\mathrm{:}{A}_{1},\mathrm{\dots},{x}_{n}\mathrm{:}{A}_{n})$ must be well-formed; thus $\mathrm{\U0001d5bc\U0001d5cd\U0001d5d1}$-ext does not need to hypothesize well-formedness of the context to the left of ${x}_{n}$.)

Title | A.2.1 Contexts |
---|---|

\metatable |