Fabian Ruch, Thesis defense, Computer science and engineering
Groupoid-Valued Presheaf Models of Univalent Type Theory
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.
Faculty opponent is Associate Professor Rasmus Ejlers Møgelberg,
Computer Science Department, IT University of Copenhagen, Denmark
Link to the full text version on the thesis
HC3, lecture hall, Hörsalar HC, Campus Johanneberg
25 November, 2022, 13:15
25 November, 2022, 15:30