Publications
Papers
The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations — Daniel Gratzer, Håkon Gylterud, Anders Mörtberg, Elisabeth Stenholm. Preprint 2024.
Univalent Material Set Theory — Håkon Robbestad Gylterud, Elisabeth Stenholm. Preprint 2023.
Master’s thesis
Formalizing Cartesian Cubical Sets in UniMath. Awarded the Mittag-Leffler prize for excellent master’s theses at Stockholm University. Defended March 2020. Supervisor: Anders Mörtberg.
Bachelor’s thesis
An Introduction to Algebraic Geometri and Bezout’s Theorem. Defended June 2018. Supervisor: Gregory Arone.
Talks
The Category of Iterative Sets in HoTT — Daniel Gratzer, Håkon Gylterud, Anders Mörtberg, Elisabeth Stenholm. Presented at HoTT/UF 2023.
Non-wellfounded Sets in HoTT — Håkon Robbestad Gylterud, Elisabeth Stenholm. Presented at HoTTEST, November 2023.
Code
Co-founder of the Agda Unimath library — the currently largest Agda library of formalised mathematics from the univalent point of view.
Set Theory in Homotopy Type Theory — an Agda formalisation of set theory in homotopy type theory.
Ongoing education
PhD candidate in Programming Theory at the University of Bergen. Supervisors: Håkon Robbestad Gylterud (Apr 2020 – Nov 2023), Anders Mörtberg (Dec 2023 –).
Degrees
Master of Science with main field of study: Mathematics. Issued at Stockholm University in April 2020.
Bachelor of Science with main field of study: Mathematics. Issued at Stockholm University in November 2018.