Context (Type Theory)

Definition

A context is an ordered list of variable assignments that record the assumed types of free variables. It is typically denoted by the Greek letter $\Gamma$.

Structure

A context is formed by a sequence of judgements $(x_1:A_1,x_2:A_2,\dots ,x_n:A_n)$. In dependent type theory, the type $A_i$ of a variable may depend on the variables $x_1,\dots ,x_{i-1}$ declared previously. A judgment $\Gamma ⊢a:A$ signifies that under the assumptions in $\Gamma$, $a$ is a valid term of type $A$.

Inference Rules

$$\begin{array}{r}\frac{}{\cdot \mathbf{con}}\frac{\Gamma ⊢\sigma \mathbf{type}x\in FV(\Gamma ,\sigma )}{(\Gamma ,x:\sigma )\mathbf{con}}\end{array}$$

Substitution

$$\frac{\Gamma ,x:A,\Delta ⊢\mathcal{J}\Gamma ⊢t:A}{\Gamma ,\Delta [U/x]⊢\mathcal{J}[U/x]}$$

for any judgement $\mathcal{J}$.

Weakening

$$\frac{\Gamma ,\Delta ⊢\mathcal{J}\Gamma ⊢A\mathbf{type}}{\Gamma ,x:A,\Delta ⊢\mathcal{J}}$$

for any judgement $\mathcal{J}$.

See Also

• Type

References

• hott2013-book
• martin-lof1984-mltt
• nederpelt2014-type-theory
• hoffmann1997-dependent-types