Homotopy Type Theory
Principal lecturer: Dr Jon Sterling
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 are useful but not required.
timetable
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).