MA 334: Introduction to Homotopy Type theory

Course Description

This course introduces homotopy type theory, which provides alternative foundations for mathematics based on deep connections between type theory, from logic and computer science, and homotopy theory, from topology. This connection is based on interpreting types as spaces, terms as points and equalities as paths. Many homotopical notions have type-theoretic counterparts which are very useful for foundations.

Such foundations are far closer to actual mathematics than the traditional ones based on set theory and logic, and are very well suited for use in computer-based proof systems, especially formal verification systems. We will use the Lean Theorem Prover in this course. Note that the latest version (Lean 3) doen not support Homotopy Type Theory (yet), so you must use Lean 2.

Prerequisites

Basic topology and mathematical maturity will be assumed. Some familiarity with algebraic topology will be helpful, as will some familiarity with programming in a functional language. This course has a flavour very different from typical mathematics courses, so open-mindedness and willingness to learn alien concepts is essential.

Project

The project for this course will be to formally prove a body of mathematics in Homotopy Type Theory in the Lean theorem prover. This will be judged on the basis of

References

Course Details