Formalising Display Map Categories in Univalent Foundations

Csanad Farkas


Date: Wed, August 27, 2025
Time: 10:00
Room: Building 22, F 206
Note: This is a MSc thesis defense


A display map category, originally just called a class of display maps with a stability condition, can be used to model dependent type theory. There are several other constructions on categories that can serve a similar purpose, such as comprehension categories. In fact, the similarity of such concept has been well-known, and there even have been comparisons made using bicategories of such categorical notions.

In this thesis, I aim to formalise one such comparison, and implement it in a proof assistant. In order to do this, I needed to formalise display map categories, some related concepts, to then construct their bicategory, and show the comparison as a pseudofunctor into the bicategory of comprehension categories. The formalisation has been done using Univalent Foundations, while the implementation has been completed using Rocq, and more specifically the UniMath library.


Previous: Maria Khakimova |
Next: