A seminar talk presented at The Antwerp Algebra Colloquium

Abstract

In 1874, (naive/Cantorian) set theory was introduced by G. Cantor which revolutionized the world of mathematics. However, not long after that, this theory gave rise to several contradictions, likeRussell’s paradox. A well-know solution is to work in Zermelo-Fraenkel set theory, but this is not the only formal system in which one can formalize mathematics. In this talk, the audience is introduced totype theory which is another formal system (introduced by B. Russell in 1903) which was also designed/introduced to overcome the paradoxes of naive set theory.

Although (Zermelo-Fraenkel) set theory is widely used, there are some unpleasant features which type theory does not satisfy. Everything in set theory is a set, the set of natural numbers is defined (very cumbersomely) as {∅, {∅}, , · · · }, a function is defined as a subset of the powerset, etc. However, an ordinary mathematician never uses these specific definitions and we take these notions as primitive, instead of “special cases”. In type theory, everything is a type and we have some (primitive) type constructors from which every mathematical structure can be specified as a type together with rules which expresses how the elements should look like instead of giving a concrete construction. As a consequence, type theory can be formalized in a computer as a programming language (which are called proof assistents).

In this talk, we start by introducing what types are and two perspectives which one can take to reason about types (i.e.Curry–Howard correspondence and Homotopy type theory). Then we go in detail how some of the most common type constructors are defined and how these correspond with the different perspectives on types. In the rest of the talk, it is illustrated how one formalizes mathematics using type theory, how such a formalization of mathematics can be implemented using a proof assistent (by the Curry–Howard correspondence) and lastly, we dive a little bit deeper in the realm on Homotopy type theory with the purpose of giving some intuition between type theory (∞-)category theory.