(Figure from the HoTT book, Creative Commons BY-SA 3.0.)
So are there any problems with conventional foundations as in logic and set theory? Recall that logic describes the laws of formal deduction and reasoning. Set theory, on the other hand, is formulated within logic and provides axioms for collections of objects. Although these conventional foundations work and all other mathematics can be developed in terms of them, they do have several issues which are not present in the type-theoretic foundations of mathematics that we discuss. For example, in conventional set-theoretic foundations, every mathematical object is necessarily a set, which leads to meaningless expressions and questions like 'is 3 ∈ π?' In type theory, on the other hand, every mathematical object has a 'type' associated to it, and the corresponding typing rules guarantee that all mathematical expressions are sensible. For example, if the type of a variable x is 'natural number' and the type of y is 'string of letters', then x+y is an expression which cannot be formed in type theory.
In this course, you will learn about type-theoretic foundations of mathematics. Among other things, you will understand how to unify the roles of logic and set theory into one coherent whole. It will also become clear why type theory is the basis of programming languages and interactive theorem provers like Coq, in which mathematical theorems have been formalized and verified by computers. The particular flavour of type theory that we will explain is the new Homotopy Type Theory (HoTT), which is currently being developed by HoTT people. HoTT brings homotopy theory to the lowest foundational level, much before topological spaces or real numbers. This allows the formulation of the univalence axiom, which roughly states that isomorphic objects are equal and thereby formalizes the common mathematical practice of identifying isomorphic objects. With the univalence axiom, HoTT turns into Univalent Foundations of Mathematics.
So if you're fascinated by mathematical elegance and would like to learn new ways of understanding and doing mathematics, then be welcome! This course is likely to shape your mathematical thinking even if you keep doing mathematics in conventional foundations.
In this course, we will roughly follow the material of the recently published and freely available HoTT book. Further generally useful resources include a discussion on the n-Category Café, an introductory paper by Pelayo and Warren, the MSc thesis of Egbert Rijke, a minicourse by Mike Shulman and the HoTT blog. Finally, there is a collection of videos of lectures!
You may also want to look at our lecture notes, which start at a more elementary level than the book and lead up to it. License: CC BY-SA 3.0. Any feedback will be welcome!
We explain the irrelevance of set-theoretic foundations for mathematical practice. This is related to the philosophy of structuralism, which is one of the key ideas implemented in univalent foundations based on HoTT. We will showcase some of the features of HoTT, for example how to define the circle and other spaces at a very fundamental level without having a notion of set, topology, or real numbers.
Starting with the technical details, we introduce some of the basic concepts of type theory: a collection of inference rules forming a trivial type theory; together with the fules of function types, this forms the (simply) typed lambda calculus with function types only.
We discuss the philosophy of constructivism and how it leads to the identification of propositions as types and proofs as algorithms. This is knows as the Curry-Howard correspondence. This correspondence is of central importance for type-theoretic foundations. We explain why the law of excluded middle cannot be derived from the inference rules.
Coq files for illustration: N_arithmetic_topic1.v, N_ordering_topic1.v, lawvere_topic2.v, composition_topic3.v.
Exercises: assignment, solutions.
We discusses the "type of all types", which is made precise by the notion of universes. Also, any foundations of mathematics has to introduce universal and existential quantifiers. In type-theoretic foundations, these are given by dependent products and dependent sums, which play the role of the quantifiers under the Curry-Howard correspondence.
Induction and recursion over the natural numbers are fundamental in all of mathematics. However, these methods are not specific to the natural numbers at all! We will show that they make sense for all inductive types and that many mathematical objects can be constructed as inductive types, e.g. the Booleans or the collection of all lists over a given alphabet.
Exercises: assignment, solutions.
These are among the most important inductive types since they define the very notion of equality. We introduce identity types and discuss the two variants of their induction principle and explain why two things can be equal in more than one way. Upon interpreting types as spaces and elements of a type as points of a space, the elements of an identity type correspond to paths in the space.
We give some examples of how to use identity types and propositional equality and also develop their general theory. Just as paths in a space, elements of identity types can be composed and inverted. Moreover, one can also consider identity types over identity types. In this way, every type carries the structure of a higher groupoid. Equalities can also be used to transport elements from one type in a type family to another.
Coq files for illustration: using_identity_types_topic7.v, discriminate_topic7.v, lift_topic7.v.
We define when two functions are homotopic and when two types are equivalent. Equivalences are the HoTT variant of isomorphisms.
Exercises: assignment, solutions.
We show things of the following form: two elements of a cartesian product are equal if and only if both components are equal; similarly, any two elements of the unit type are equal. The "if and only if" here is precisely the notion of equivalence introduced before. In other cases, like for function types or for the universe, characterizing identity types requires an additional axiom: the univalence axiom states that the identity type between types A and B (as elements of the universe) is equivalent to the type of equivalences between A and B. This is the central new ingredient of HoTT!
Coq file for illustration: characterizing_identities_topic9.v.
A type is a mere proposition if any two of its elements are equal; having an element of a mere proposition does not give any information other than that the mere proposition is true, so that one can think of the element as a "mere" proof. A type is a set if any two paths between any two elements are equal, so that there is no non-trivial homotopy. Finally, a type is contractible if it is equivalent to the unit type. We discuss these concepts, how they relate to they other, and their significance for the law of excluded middle and the axiom of choice.
Coq files for illustration: universe_not_a_set.v, ishprop_biinv.v.
Higher inductive types, for example the circle, generalize inductive types by allowing constructors which not only return elements of the type itself, but also paths between these elements. Higher inductive types are not only ubiquitous in homotopy theory, but are also useful when taking the quotient of a set (or other type) with respect to an equivalence relation. We show that the fundamental group of the circle is the integers.
Coq file for illustration: circle_properties.v.
Ideas for course projects are here.