Skip to main content

Peter LeFanu Lumsdaine: Large cardinals in type theory

Time: Wed 2022-11-30 10.00 - 12.00

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

Participating: Peter LeFanu Lumsdaine, Stockholm University

Export to calendar

Abstract

This will be an expository seminar, surveying results of Dybjer, Setzer, and Palmgren (and possibly others).

Large cardinals are a mainstay of classical set theory, and are often thought of as its of little interest beyond it. However, at least some large cardinal principles turn out — unsurprisingly, in hindsight — to correspond to natural largeness conditions on universes in type theory, phrased in terms of closure under various type-forming constructions. I will introduce and survey the best-understood such connections and their implications, in particular the correspondence (established by Dybjer and Setzer) between Mahlo cardinals and universes closed under formation of inductive-recursive types.