Homotopy Type Theory & Univalent Foundations

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.

Pre-registration evaluation form 

Students who are interested in taking this module will be asked to complete a pre-registration evaluation form to determine whether they have sufficient background to take the module. 

This will take place during the week Monday 11 August - Friday 15 August. 

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.