A.0 Preliminaries

In http://planetmath.org/node/87533Chapter 1, we presented the two basic judgments of type theory. The first, $a:A$, asserts that a term $a$ has type $A$. The second, $a\equiv b:A$, states that the two terms $a$ and $b$ are judgmentally equal at type $A$. These judgments are inductively defined by a set of inference rules described in sec:syntax-more-formally.

To construct an element $a$ of a type $A$ is to derive $a:A$; in the book, we give informal arguments which describe the construction of $a$, but formally, one must specify a precise term $a$ and a full derivation that $a:A$.

However, the main difference between the presentation of type theory in the book and in this appendix is that here judgments are explicitly formulated in an ambient context, or list of assumptions, of the form

$$x_1:A_1,x_2:A_2,\mathrm{\dots },x_n:A_n.$$

An element $x_i:A_i$ of the context expresses the assumption that the variable $x_i$ has type $A_i$. The variables $x_1,\mathrm{\dots },x_n$ appearing in the context must be distinct. We abbreviate contexts with the letters $\mathrm{\Gamma }$ and $\mathrm{\Delta }$.

The judgment $a:A$ in context $\mathrm{\Gamma }$ is written

$$\mathrm{\Gamma }⊢a:A$$

and means that $a:A$ under the assumptions listed in $\mathrm{\Gamma }$. When the list of assumptions is empty, we write simply

$$⊢a:A$$

or

$$\cdot ⊢a:A$$

where $\cdot$ denotes the empty context. The same applies to the equality judgment

$$\mathrm{\Gamma }⊢a\equiv b:A$$

However, such judgments are sensible only for well-formed contexts, a notion captured by our third and final judgment

$$(x_1:A_1,x_2:A_2,\mathrm{\dots },x_n:A_n)\mathrm{𝖼𝗍𝗑}$$

expressing that each $A_i$ is a type in the context $x_1:A_1,x_2:A_2,\mathrm{\dots },x_{i-1}:A_{i-1}$. In particular, therefore, if $\mathrm{\Gamma }⊢a:A$ and $\mathrm{\Gamma }\mathrm{𝖼𝗍𝗑}$, then we know that each $A_i$ contains only the variables $x_1,\mathrm{\dots },x_{i-1}$, and that $a$ and $A$ contain only the variables $x_1,\mathrm{\dots },x_n$.

In informal mathematical presentations, the context is implicit. At each point in a proof, the mathematician knows which variables are available and what types they have, either by historical convention ($n$ is usually a number, $f$ is a function, etc.) or because variables are explicitly introduced with sentences such as “let $x$ be a real number”. We discuss some benefits of using explicit contexts in sec:more-formal-pi,sec:more-formal-sigma.

We write $B[a/x]$ for the substitution of a term $a$ for free occurrences of the variable $x$ in the term $B$, with possible capture-avoiding renaming of bound variables, as discussed in §1.2 (http://planetmath.org/12functiontypes). The general form of substitution

$$B[a_1,\mathrm{\dots },a_n/x_1,\mathrm{\dots },x_n]$$

substitutes expressions $a_1,\mathrm{\dots },a_n$ for the variables $x_1,\mathrm{\dots },x_n$ simultaneously.

To bind a variable $x$ in an expression $B$ means to incorporate both of them into a larger expression, called an abstraction, whose purpose is to express the fact that $x$ is “local” to $B$, i.e., it is not to be confused with other occurrences of $x$ appearing elsewhere. Bound variables are familiar to programmers, but less so to mathematicians. Various notations are used for binding, such as $x\mapsto B$, $\lambda x.B$, and $x.B$, depending on the situation. We may write $C[a]$ for the substitution of a term $a$ for the variable in the abstracted expression, i.e., we may define $(x.B)[a]$ to be $B[a/x]$. As discussed in §1.2 (http://planetmath.org/12functiontypes), changing the name of a bound variable everywhere within an expression (“$\alpha$-conversion”) does not change the expression. Thus, to be very precise, an expression is an equivalence class of syntactic forms which differ in names of bound variables.

One may also regard each variable $x_i$ of a judgment

$$x_1:A_1,x_2:A_2,\mathrm{\dots },x_n:A_n⊢a:A$$

to be bound in its scope, consisting of the expressions $A_{i+1},\mathrm{\dots },A_n$, $a$, and $A$.

Title	A.0 Preliminaries