Mini-course by Ulrik Buchholtz

We are delighted to welcome Ulrik Buchholtz (Functional Programming Lab, School of Computer Science, The University of Nottingham) for a mini-course on synthetic homotopy theory.

Introduction to Synthetic Homotopy Theory

We’ll cover topics in synthetic homotopy theory using homotopy type theory/univalent foundations. First, we’ll give a brief overview of Martin-Löf type theory and an intuitive picture of its interpretation in spaces qua infinity-groupoids. This interpretation motivates Voevodsky’s definition of contractible types, equivalences, homotopy n-types, n-connected types, and the univalence axiom.

Next, we cover homotopy pushouts as a new type constructor, including variations such as the circle, suspensions, cofibers, joins, and smash products. We’ll look at the type-theoretic formulation of homotopy groups, and the long exact sequence given by a map, leading to the calculation of some homotopy groups.

The last lecture will cover the zigzag construction of the path spaces of pushouts, leading to a type-theoretic proof of the Blakers–Massey connectivity theorem. Time permitting, we can touch on other aspects of synthetic homotopy theory, according to the interests of the participants.

Practical information

Dates: Wednesdays 25 March, 1 April and 8 April 2026
Times: 4.00 pm to 6.00 pm
Location: Room B405, LAGA, Sorbonne Paris Nord University (99 Av. Jean Baptiste Clément, 93430 Villetaneuse)
Participation: The course is available in a hybrid format, either in person or online, via the link here : https://bbb.math.univ-paris13.fr/b/chr-hyw-0rb-jz4
Lecturer’s personal website: https://ulrikbuchholtz.dk/