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 | Enhancing Proof Assistant Error Messages with Hints: A User Study
Next: