Groupoid-Valued Presheaf Models of Univalent Type Theory

Beskrivning av avhandlingen:

In computer science and mathematics formal languages are used to express programs, structures and proofs in a precise way. One way to study those languages and the concepts they express is to construct models of them. Models in this context are like translations from a source language to a target language. They can be used to give meaning to or explain concepts expressed in the source language, to show properties or the limits of what can be expressed, to justify additions to the source language, or to express concepts in the target language using the concepts of the source language when that is more convenient or general.

This thesis is concerned with models of a language called dependent
type theory. More specifically, it is concerned with models of dependent type theory that satisfy the univalence axiom. Dependent type theory is a language for all three concepts mentioned above: programs, structures and proofs. The univalence axiom is an addition to the language that says that equivalent structures are identified. This thesis presents a technique to construct new univalent models from old ones, and applies that technique to construct presheaf models of univalent type theory. Presheaf models play a significant role in all the uses mentioned above.

Fakultetsopponent:

Docent Rasmus Ejlers Møgelberg, Computer Science Department, IT University of Copenhagen, Danmark

Betygsnämnd:

• Docent Olivia Caramello, University of Insubria, Como, Italien,
• Docent Bas Spitters, Department of Computer Science, Aarhus University, Danmark
• Professor Thomas Streicher, Logik arbeitsgebiet, Technische Universität Darmstadt, Tyskland

Länk till fulltextversion av avhandlingen