Skip to main content

Peter LeFanu Lumsdaine: The cumulative hierarchy in type theory

Time: Wed 2023-02-08 10.00 - 12.00

Location: Albano house 1, floor 3, Room U (Kovalevsky)

Participating: Peter LeFanu Lumsdaine, Stockholm University


In ZF(C) and similar material set-theoretic foundations, the cumulative hierarchy of iterative sets provides the arena in which all mathematics takes place. In other foundations, is place is less central; but it still exists, as a rich and useful structure.

In this talk, I will survey several treatments of the cumulative hierarchy and variants in type theory and related settings, including some or all of:

- Aczel’s type of iterative sets

- Palmgren’s applications of this in “From type theory to setoids and back”

- Gylterud’s adaptation of it to multisets

- Moerdijk and Joyal’s “Algebraic set theory” characterisation of the cumulative hierarchy

- the HoTT book’s presentation of the cumulative hierarchy as a higher inductive type.