Abstract
In dependent type theory universes play a central role. It is sometimes discussed whether they are “open” or “closed”. On the one hand in a proof assistant such as Agda they are open in that you can add new data types in them at any point in your development. On the other hand, universes à la Tarski are special kinds of inductive-recursive definitions, which means that they closed and admit an induction principle. With this as a starting point I will discuss various aspects of universes.
Talk Details
Speaker: Peter Dybjer (Chalmers University of Technology, Sweden)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Wednesday 17 December 2025
Time: 11:25
Slides: Available
Key Topics
- Dependent type theory
- Universes
- Tarski-style universes
- Inductive-recursive definitions
- Agda proof assistant
- Type theory foundations
- Induction principles
- Open vs closed universes
Related Work
- Tarski’s work on universes
- Inductive-recursive definitions theory
- Agda implementation