Homotopy Type Theory & Univalent Foundations
Taken by: MPhil ACS, Part III
Code: L313
Term: Michaelmas
Hours: 16 (8 x 2-hour lectures)
Format: In-person lectures
Class limit: max. 15 students
Prerequisites: Familiarity with basic logic, naïve set theory, and typed λ-calculus. Students will have to pass an entry test to ensure sufficient Mathematical background.
timetable
Aims
Homotopy type theory/univalent foundations is a new foundations for general mathematics in which equality is relaxed to include symmetry, and sets arise as a special case of infinite-dimensional structures called homotopy types. This course introduces the basic notions of univalent foundations (dependent types, identity types, equivalences, truncation levels, the univalence axiom, classifying types, and fundamental groups). After taking this course, a student would be able to read and participate in the current discourse on the frontiers of univalent foundations.
Syllabus
Dependent types I. Dependent type theory, judgemental equality, dependent function and pair types, fibres, natural numbers. Identity types, transport, groupoidal structure of types, uniqueness of singletons; universes. Dependent Types II. Formal dependent types in the Agda proof assistant: inductive data types, dependent record types, universes, observational equivalence of natural numbers. Univalent foundations I. Homotopies, equivalences, contractible types, propositions, sets, n-truncated types, n-truncated maps, closure properties of n-truncated types. Hedberg's theorem. Univalent foundations II. Reflexive graphs, univalent reflexive graphs, fundamental theorem of identity types, function extensionality and the univalence axiom. Displayed reflexive graphs and the structure identity principle. Univalent foundations III. Consequences of function extensionality and univalence: products and sums of truncated types. Coherence for equivalences and truncation-level proofs. Relating equivalences to contractible maps. Univalent foundations IV. Fibrations vs. families of types; propositional truncations, image factorisations; set truncations and connected types; classical mathematics in univalent foundations. Symmetry I. Groups in univalent foundations, the structure identity principle for groups, the Eckmann–Hilton argument; concrete groups and classifying types in univalent foundations. Symmetry II. The circle, universal cover of the circle, descent data over the circle, the universal property of the integers, the fundamental group of the circle.
Learning Outcomes
Dependent type theory as a vernacular for informal mathematics; characterising identifications of algebraic structures using the univalence axiom; symmetry in univalent foundations and a taste of synthetic homotopy theory.
Assessment
- a graded exercise sheet (25% of the final mark)
- a take-home test (75%)
Recommended Reading
1. Egbert Rijke. Introduction to Homotopy Type Theory.
2. Martín Hötzel Escardó. Introduction to Univalent Foundations
of Mathematics with Agda.
3. The Univalent Foundations Program. Homotopy Type Theory:
univalent foundations of mathematics.