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
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.