A.0 Preliminaries

In http://planetmath.org/node/87533Chapter 1, we presented the two basic judgmentsof 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 judgmentallyequalat type $A$ . These judgments are inductively defined by a set ofinference rules described in \\autorefsec:syntax-more-formally.

To construct an element $a$ of a type $A$ is to derive $a : A$ ; in the book, wegive 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 bookand in this appendix is that here judgments are explicitlyformulated in an ambient context,or list of assumptions, of the form

x_{1}:A_{1},x_{2}:A_{2},\\dots,x_{n}:A_{n}.

An element $x_{i}:A_{i}$ of the context expresses the assumption that thevariable $x_{i}$ has type $A_{i}$ . The variables $x_{1},\\ldots,x_{n}$ appearing inthe context must be distinct. We abbreviate contexts with the letters $\\Gamma$ and $\\Delta$ .

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

\\Gamma\\vdash a:A

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

\\vdash a:A

\\cdot\\vdash a:A

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

\\Gamma\\vdash 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},\\dots,x_{n}:A_{n})\\ \\mathsf{ctx}

expressing that each $A_{i}$ is a type in the context $x_{1}:A_{1},x_{2}:A_{2},\\dots,x_{i-1}:A_{i-1}$ . In particular, therefore, if $\\Gamma\\vdash a:A$ and $\\Gamma\\ \\mathsf{ctx}$ , then we know that each $A_{i}$ contains only the variables $x_{1},\\dots,x_{i-1}$ , and that $a$ and $A$ contain only the variables $x_{1},\\dots,x_{n}$ .

In informal mathematical presentations, the context isimplicit. At each point in a proof, the mathematician knows whichvariables are available and what types they have, either by historicalconvention ( $n$ is usually a number, $f$ is a function, etc.) orbecause variables are explicitly introduced with sentences such as“let $x$ be a real number”. We discuss some benefits of using explicitcontexts in \\autorefsec:more-formal-pi,\\autorefsec:more-formal-sigma.

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

B[a_{1},\\dots,a_{n}/x_{1},\\dots,x_{n}]

substitutes expressions $a_{1},\\dots,a_{n}$ for the variables $x_{1},\\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., itis not to be confused with other occurrences of $x$ appearingelsewhere. 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 thesubstitution 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 veryprecise, an expression is an equivalence class of syntactic formswhich 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},\\dots,x_{n}:A_{n}\\vdash a:A

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