Homotopy type theory: Univalent Foundations of Mathematics

ECTS credits: 7.5 ECTS

Language: English

Level of course: PhD

Time of year: Autumn 2015

Contact hours: 3hr lectures/seminar + 8hr preparation per week, 40hr final assignment. Total 194hr

Objectives of the course: Homotopy type theory is a new branch of mathematics and computer science that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. It touches on topics as seemingly distant as algebraic topology, the algorithms for type checking, and the definition of weak infinity groupoids. Homotopy type theory offers a new univalent foundation of mathematics, in which a central role is played by Voevodsky's univalence axiom and higher inductive types. The former provides a flexible formal framework for working with equivalences. The latter greatly enhances the expressiveness of type theory by including general homotopy colimits. This allows the concise presentation of algebraic topology, but also advance data structures from computer science. The univalent foundations are being developed as a viable alternative to set theory as the `implicit foundation' for the unformalized mathematics done by most mathematicians. At the same time, computer proof assistants are now standard tools in software verification. Proof assistants based on type theory, such as Coq and agda, are among the most successful ones in interactive theorem proving. Likewise, in functional programming there is a push towards more expressive type systems, including dependent types. Homotopy type theory is closely intertwined with both these topics. The course is intended as an introduction to the basics of the univalent foundations.

The objective of this course is:

• To reach up to the research level in homotopy type theory.
• To be familiar with the syntax and semantics of the univalent foundations.
• To obtain a basic understanding of computer formalized proofs in the univalent foundation

Learning outcomes and competences:

• Develop mathematics in the univalent foundations
• Read research papers in the categorical semantics of type theory
• Read and write computer proofs in homotopy type theory. Specifically, we will use the Coq proof assistant.
• Present and explain the acquired material to others

Compulsory programme: None

Course contents: The course will be held in a lecture/seminar style. Each week will include general lecture by Bas Spitters and a seminar presentation on a specific topic by a PhD-student.

Prerequisites: Basic Type theory, Category theory, Familiarity with computer formalized proofs. Not strictly necessary, but useful: basic familiarity with homotopy theory and algebraic topology

Name of lecturer:Dr. Bas Spitters

Type of course/teaching methods: Lectures, Seminar, Exercises

Literature:

• Homotopy Type Theory: Univalent Foundations of Mathematics. Information available at: here
• Research papers on the semantics of homotopy type theory

Course assessment: Each student has to give two presentations one on syntax, one on semantics. The former will be material from the book. The latter from a research article. In addition to this the students can choose one of the following assignments:

• A collection of completed exercises
• A computer formalization project
• A report on a small research project

Time and Place:
Tue 10-12: Tur 014
Thu 13-15: Ada 018

Registration: Deadline for registration is 1 August 2015. Information regarding admission will be sent out no later than 8 August 2015.

For registration: send an e-mail to spitters at cs you know where detailing your prerequisites, in particular.