Type theory

1. Type theory#

1.1. Outline#

The working mathematician is familiar with the set-theoretic foundation of mathematics. However, Lean and many other proof assistants use a different formalism known as type theory. This is because type theory is quite close to how mathematics is actually done, and because type theory can be used simultaneously as a programming language and a foundation of mathematics.

In this lecture we shall review the basics of type theory, starting from the idea that we are “just reformulating” set theory. While this gives a coherent view of what type theory is about (namely sets), one should keep in mind that it is not the only possible coherent view. A notable alternative is homotopy type theory.

Traditional axiomatizations of set theory, for instance the Zermelo-Fraenkel set theory, are based on first-order logic and describe sets in terms of existence axioms. Type theory is closer to algebra, because it describes what sets are in terms of constructions, operations and equations.

1.2. Reading material#

At this point you should read the following material:

If you would like to see how the “real-world” type theory of Lean is defined, have a look at:

1.3. Video and class notes#

Contents