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.