Skip to main content

PhD Course: Homotopical Models of Type Theories

Time: Mon 2021-09-06 11.00

Location: Zoom, meeting ID: 669 6981 2286

Lecturer: Peter LeFanu Lumsdaine and Anders Mörtberg

See course web page  for full details.


The initial organisational meeting will be at 11:00 on Monday 6 Sep, over Zoom . If you’re interested in participating, please let us know by email (, and/or turn up to the meeting. Lectures may be online or in-person depending on the number/preferences of interested students.


Homotopy type theory, relating Martin-Löf’s dependent type theory to homotopy theory, was originally based in large part on Voevodsky’s model of type theory in simplicial sets. More recently, models in cubical sets have turned out to enjoy various computational and technical advantages; meanwhile, models have also been given in large classes of suitably-structured (∞,1)-categories, although these are as yet less well understood. From the point of view of logic, this offers new ways to understand equality (in the form of Martin-Löf's identity type); from the point of view of topology, it provides a powerful language for reasoning axiomatically about spaces.

This course will give an introduction to homotopy type theory, with a focus on its models. We will not assume prior knowledge of type theory, but will start with a brief introduction focusing on homotopical aspects. Similarly, we will not assume prior experience of homotopical algebra, but will introduce tools as they are required.


  • Core category theory (essential)
  • Some basic algebraic topology (highly desirable)
  • Some acquaintance with dependent type theory (helpful)
Belongs to: Department of Mathematics
Last changed: Aug 25, 2021