Peter LeFanu Lumsdaine: Large cardinals in type theory

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.