PhD thesis

From 2015 to 2020 I have worked on a PhD on Univalent Type Theory under the supervision of Martín Escardó and Benedikt Ahrens. You can find the final version of my PhD thesis here.

I wrote formalized proofs of part of my thesis in Coq. This work is now integrated in the HoTT library.

Part of my work has also been published as an article (preprint on the arXiv), to appear in the MSCS Special Issue on Homotopy Type Theory and Univalent Foundations.