Abstract

Abstract: Homotopy Type Theory (HoTT) is a new field of research combining constructive type theory, homotopy theory, and higher category theory, with applications to the formalization of mathematics. This survey talk will introduce the basic theory, explain the surprising connection between the foundations of mathematics and algebraic topology, and survey some of the resulting developments in formal theorem proving in the years since its discovery.

About the speaker: Steve Awodey is a Royal Society Wolfson Visiting Fellow at Cambridge CST for 2026-7. In real life he is the Dean’s Chair of Logic at Carnegie Mellon University.

Link to join virtually: https://cam-ac-uk.zoom.us/j/89473073451

A recording of this talk is available at the following link: https://www.cl.cam.ac.uk/seminars/wednesday/video/

This talk is being recorded. If you do not wish to be seen in the recording, please avoid sitting in the front three rows of seats in the lecture theatre. Any questions asked will also be included in the recording. The recording will be made available on the Department’s webpage