Goal
Martin-Löf Type Theory provides a powerful syntax in which to express mathematical concepts and formalise them in a programming language. Combined with homotopy theory, it also provides a geometric framework for proof theory that is both intuitive and helpful. The goal of this workshop is to present an introduction to these topics for mathematicians, emphasising the type-theoretic aspects and the synthetic approach.
Registration deadline: 24 May 2026 (Registration form).
Lecturers
- Felix Cherubini (Augsburg).
- Paige North (Utrecht).
Speakers
- Fernando Chu-Rivera (Utrecht).
- Gabriella Clemente (Paris).
- Tom de Jong (Nottingham).
- Meven Lennon-Bertrand (Paris).
- Maria Emilia Maietti (Padova).
- Hugo Moeneclaey (Gothenburg).
Schedule
The workshop will consist of two lecture series (3 x 1h) and six research talks (1h).
| Day 1 | Day 2 | Day 3 |
|---|---|---|
| Paige North (1) | Paige North (2) | Felix Cherubini (3) |
| Milly Maietti | Felix Cherubini (2) | Paige North (3) |
| Lunch break | Lunch break | |
| Felix Cherubini (1) | Free afternoon | Hugo Moeneclaey |
| Tom de Jong | Meven Lennon-Bertrand | |
| Gabriella Clemente | Fernando Chu |
Program
Lectures
The definition of the basic objects of algebraic geometry, schemes, requires a stack of notions that has to be unfolded and reconstructed a lot. In Synthetic Algebraic Geometry (SAG), a scheme is just a set with a property and morphisms of scheme are just functions of sets.
To make this work, we introduce three axioms, which are incompatible with the axiom of choice. One of the axioms, called Zariski-local choice (ZLC), introduces a new choice principle related to the Zariski-topology, which relates affine schemes to objects which are not sets, but higher types. We have access to the latter by reasoning in homotopy type theory.
We will give an introduction to the constructive algebra needed in SAG and present the axioms of SAG. With the axioms, we will define schemes and construct basic examples. We will show the role of ZLC in making basic topological properties of schemes work and finally show the original motivation behind ZLC: Higher types can be used to define cohomology groups of schemes and with ZLC it is possible to recompute classical results without the usual technicalities.
The Equivalence Principle is an informal principle asserting that equivalent mathematical objects have the same properties. For example, group theory has been developed so that isomorphic groups have the same group-theoretic properties, and category theory has been developed so that equivalent categories have the same category-theoretic properties (though sometimes other, ‘evil’ properties are considered). Vladimir Voevodsky established Univalent Foundations (also known as homotopy type theory) as a foundation of mathematics (based on dependent type theory) in which the Univalence Principle, and thus the Equivalence Principle, for types (the basic objects of type theory) is a theorem. Later, versions of the Equivalence Principle for set-based structures such as groups and categories were shown to be theorems in Univalent Foundations.
In joint work with Ahrens, Shulman, and Tsementzis, we formulate and prove versions of the Equivalence Principle for a large class of categorical and higher categorical structures in Univalent Foundations. Our work encompasses (higher) categorical structures such as bicategories, dagger categories, opetopic categories, and more.
The Equivalence Principle in Univalent Foundations rely on the fact that the basic objects – the types – can be regarded as spaces. That is, Univalent Foundations can be viewed as an axiomatization of homotopy theory and as such is closely related to Quillen model category theory. Univalent Foundations can also be viewed as a foundation of mathematics based not on sets, but on spaces. It is the homotopical content of this foundation of mathematics that allows us to prove something like the Equivalence Principle, something which is not possible in set-based foundations of mathematics, such as ZFC.
I will begin the lecture series with a whirlwind introduction to Univalent Foundations, and then continue on to explain how we can prove the equivalence principle in it for various structures. If time allows, I will also talk about work to develop an extension of Univalent Foundations in which the basic objects are not spaces but higher categories.
Talks
Synthetic differential geometry (SDG) is an axiomatic version of differential geometry, whose context is a smooth topos instead of the category of smooth manifolds. After covering the basics of SDG, I will talk about recent developments in synthetic differential calculus from the joint work https://hal.science/hal-05555752/document. I will then discuss smooth toposes through examples of well-adapted models, as well as work in progress in the area that is a collaboration with Riccardo Brasca and Joël Riou. Time permitting, I will explain some of the peculiarities of formalizing SDG in Lean.
In the first part of this talk, I will present the 1-groupoid model of MLTT. This model validates a restricted version of the univalence axiom, which can be used to develop 1-groupoid theory synthetically. The relation to the ∞-groupoid model of HoTT will be briefly sketched. In the second part of the talk, I will motivate Directed Type Theory as a language for developing category theory synthetically and sketch some work in progress (joint work with Paige R. North) in this direction https://arxiv.org/abs/2602.17480.
I will explain how we can develop homotopy theory synthetically in homotopy type theory (HoTT). As a particular example, I will focus on epimorphisms, characterizing these via suspensions, and present examples and applications in group theory via the identification of groups with certain higher types.
This is based on a paper with Ulrik Buchholtz and Egbert Rijke: Epimorphisms and Acyclic Types in Univalent Foundations. In: The Journal of Symbolic Logic (2025), pp. 1–36. doi: 10.1017/jsl.2024.76.
In the synthetic viewpoint on type theory, one works inside a particular type theory, whose rules capture the features of the mathematical objects of interest. However, type theory itself can be studied as a mathematical object in its own right. This is necessary to formally explain how the synthetic language relates to the objects it is intended to capture, but is more generally a rich field of mathematical investigations. My talk will be an introduction to these investigations.
I will present Generalised Algebraic Theories, one of the most popular formal definition of what a type theory is; introduce the closely related notions of Categories with Families and Natural Models, two standard ways of capturing when a given structure can interpret a type theory; and explain how one can think of syntax formally in this setting. Time allowing, I might also talk a bit about how all of this relates to proof assistant implementation.
Dependent type theories, such as Martin-Löf Type Theory and Homotopy Type Theory, have provided a solid basis for the development of formal mathematics, that is, mathematics formalized within proof assistants.
In this talk, based on recent results in [1,4], we describe some principles that distinguish Martin-Löf Type Theory and Homotopy Type Theory within the landscape of foundations of mathematics, and in particular within constructive mathematics. Our analysis is carried out by referring to a third foundation, called the Minimalist Foundation, developed in [2,3] as a common core underlying the main foundational systems for mathematics.
These distinguishing principles include certain forms of choice axioms, as well as computability and continuity principles.
[1] Contente, M. and Maietti, M. E. , “The Compatibility of the Minimalist Foundation with Homotopy Type theory.” , Theoretical Computer Science, vol. 991, p. 114421, 2024
[2] Maietti, M.E., Sambin, G.: Toward a minimalist foundation for constructive mathematics. In: L. Crosilla and P. Schuster (ed.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, no. 48 in Oxford Logic Guides, p. 91-114. OUP (2005)
[3] Maietti, M.E.: A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic 160(3), 319{354 (2009)
[4] M. E. Maietti, P. Sabelli, and D. Trotta. Effectiveness and continuity in intuitionistic quasi-toposes of assemblies. Mathematical Structures in Computer Science, vol 36, 2026