Groupoid-Valued Presheaf Models of Univalent Type Theory
Science and Information Technology
Fabian Ruch is defending his doctoral thesis for the Degree of Doctor of Philosophy in the subject Computer Science and Engineering.
Fabian Ruch is defending his doctoral thesis for the Degree of Doctor of Philosophy in the subject Computer Science and Engineering.
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.
Associate professor Rasmus Ejlers Møgelberg, Computer Science Department, IT University of Copenhagen, Danmark