What is HoTT?

Add to your list(s) Download to your calendar using vCal

• Professor Steve Awodey - Departments of Philosophy and Mathematics, Carnegie Mellon University
• Wednesday 28 January 2026, 15:05-15:55
• Lecture Theatre 1, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Ben Karniely.

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

This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory, William Gates Building
• Martin's interesting talks
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• se393's list
• yk449

Note that ex-directory lists are not shown.