# 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 \autorefsec: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}\u22a2a:A$$ |

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

$$\u22a2a:A$$ |

or

$$\cdot \u22a2a:A$$ |

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

$$\mathrm{\Gamma}\u22a2a\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{\U0001d5bc\U0001d5cd\U0001d5d1}$$ |

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}\u22a2a:A$ and $\mathrm{\Gamma}\mathrm{\U0001d5bc\U0001d5cd\U0001d5d1}$, 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 \autorefsec:more-formal-pi,\autorefsec: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}\u22a2a: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 |
---|---|

\metatable |