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

Link to zoom: https://chalmers.zoom.us/j/65941841738, password 601869

Category Thesis defence
Location: HC3, lecture hall, Hörsalar HC, Campus Johanneberg
Starts: 25 November, 2022, 13:15
Ends: 25 November, 2022, 15:30

Page manager Published: Tue 22 Nov 2022.