Homotopy Type Theory
Principal lecturers: Dr Jon Sterling, Prof Steve Awodey
Taken by: MPhil ACS, Part III
Code: L103
Term: Lent
Hours: 16
Class limit: max. 15 students
Prerequisites: The module has no formal prerequisites beyond comfort with proof-based mathematics; we encourage enrolment from students who are familiar with basic logic, naïve set theory, and typed lambda-calculus. Whatever category theory is needed will be taught in the module. Prior experience with basic homotopy theory and type theory is useful but not required.
timetable
Important Information
This module is jointly offered with the Department of Pure Mathematics and Mathematical Statistics (DPMMS). Lectures will be held in the Maths department
Aims
This lecture course will provide an introduction to Homotopy Type Theory, a new area of foundations combining homotopy theory, type theory, and higher category theory.
The course will cover the following topics:
1. Review of category theory
2. Cartesian closed categories and simple type theory
3. Locally Cartesian closed categories and dependent type theory
4. Quillen model categories and homotopy type theory
Objectives
Syllabus
Assessment
- A graded exercise sheet completed during Term (30% of the final mark).
- A viva voce examination to be conducted after the course (70% of the final mark).