1st Semester 2018/19: Computer Assisted Homotopy Type Theory in Agda

Instructors

Andrew Swan

If you are interested in this project, please contact the instructor(s) by email.

Registration through https://datanose.nl/#specialenrol, using the course code: 5314CAHT6Y

ECTS

6

Description

Martin-Löf type theory is a formal approach to mathematics based on intuitionism and constructive mathematics. In type theory every proof must be justified with computational information. For example, to show that there is a natural number with a certain property, it is necessary to show how to construct (or "compute") at least one such number. For this reason, type theory can be viewed not only as a formal theory for mathematics, but as a very high level programming language.

Homotopy type theory is a relatively new approach to type theory due to Vladimir Voevodsky, in which we focus on what is in some ways the most mysterious part of type theory: the identity types. To prove that two elements of a type are equal is to construct an element of an identity type. A key insight is that we should understand the elements of an identity type as paths between two points in a topological space. This enabled Voevodsky to transfer many existing ideas from homotopical algebra into type theory.

Proof assistants are pieces of software that help us to enter mathematical proofs into a computer in such a way that they can be verified automatically. From its very beginnings homotopy type theory has been closely associated with proof assistants, with many important results formalised electronically before they even appear on paper. Short but strange and sometimes unintuitive proofs can be quickly entered and verified automatically, while for longer proofs the computer can help structure the proof, keeping track of what still needs to be proved, and ensuring that all the pieces fit together in the end.

In this course I will introduce homotopy type theory from a computer assisted point of view using the Agda proof assistant. I will cover some basic results from homotopy type theory and show how these results can be formalised using Agda.

Organisation

The course will be split into two halves of roughly 2 weeks each. The first half will be an introduction to homotopy type theory and Agda consisting of combined lectures/lab classes. In the second half students will work on a project, formalising a theorem from homotopy type theory in Agda.

Prerequisites

Students should have general mathematical maturity and familiarity with some form of formal logic. They should also be comfortable using a computer, ideally with a little programming experience.

Some experience with homotopy type theory would be helpful, but this course can also serve as a first introduction if not. Similarly existing experience with a proof assistant is helpful but not required.

Students are expected to install Agda on their own computers (although help can be provided for this if necessary) and to bring them to lab classes.

Assessment

Pass/fail based on lab classes and project.

References

 

The Univalent Foundations Program, Homotopy Type Theory

The main Agda homepage is at http://wiki.portal.chalmers.se/agda/pmwiki.php with installation instructions at https://agda.readthedocs.io/en/latest/getting-started/installation.html