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.

25 Nov 2022
13:15 - 16:00
Room HC3, Hörsalsvägen 14, Campus Johanneberg, Gothenburg, and can also be followed via Zoom
Additional info
Link to

Good to know
Meeting passcode for Zoom: 601869

Description of the thesis:

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:

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

Grading committee:

  • Associate professor Olivia Caramello, University of Insubria, Como, Italy
  • Associate professor Bas Spitters, Department of Computer Science, Aarhus University, Denmark
  • Professor Thomas Streicher, Logik arbeitsgebiet, Technische Universität Darmstadt, Germany

Link to fulltext version of the thesis