A.2.1 Contexts


A context is a list

x1:A1,x2:A2,,xn:An

which indicates that the distinct variables x1,,xn are assumed to have types A1,,An, respectively. The list may be empty. We abbreviate contexts with the letters Γ and Δ, and we may juxtapose them to form larger contexts.

The judgment Γ𝖼𝗍𝗑 formally expresses the fact that Γ is a well-formed context, and is governed by the rules of inferenceMathworldPlanetmath {mathpar} \inferrule*[right=𝖼𝗍𝗑-emp]    𝖼𝗍𝗑 \inferrule*[right=𝖼𝗍𝗑-ext] x_1 : A_1, …, x_n-1 : A_n-1 ⊢A_n : 𝒰 _i (x_1 : A_1, …, x_n : A_n) 𝖼𝗍𝗑 with a side condition for the second rule: the variable xn must be distinct from the variables x1,,xn-1. Note that the hypothesisMathworldPlanetmathPlanetmath and conclusionMathworldPlanetmath of 𝖼𝗍𝗑-ext are judgments of different forms: the hypothesis says that in the context of variables x1,,xn-1, the expression An has type 𝒰i; while the conclusion says that the extended context (x1:A1,,xn:An) is well-formed. (It is a meta-theoretic property of the system that if x1:A1,,xn:Anb:B is derivablePlanetmathPlanetmath, then the context (x1:A1,,xn:An) must be well-formed; thus 𝖼𝗍𝗑-ext does not need to hypothesize well-formedness of the context to the left of xn.)

Title A.2.1 Contexts
\metatable