# 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

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