Publications

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations — Daniel Gratzer, Håkon Gylterud, Anders Mörtberg, Elisabeth Stenholm.

Univalent Material Set Theory — Håkon Robbestad Gylterud, Elisabeth Stenholm.

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory — Håkon Robbestad Gylterud, Elisabeth Stenholm. Preprint 2025.

Material Set Theory in Homotopy Type Theory. PhD thesis, defended 2024-11-29 at the University of Bergen.

Formalizing Cartesian Cubical Sets in UniMath. Master’s thesis, defended March 2020. Supervisor: Anders Mörtberg. Awarded the Mittag-Leffler prize for excellent master’s theses at Stockholm University.

An Introduction to Algebraic Geometri and Bezout’s Theorem. Bachelor’s thesis, defended June 2018. Supervisor: Gregory Arone.

Talks

A different way to do concurrency — Haskell’s STM monad. Invited talk at Func Prog Conf 2025

Dependent types are everywhere! Presentation at Func Prog Sweden, April 2025.

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.

Containers — an Agda library on the theory of containers.

Degrees

Philosophiae doctor (PhD) in Programming Theory at the University of Bergen. Thesis defended 2024-11-29 at the University of Bergen. Supervisors: Håkon Robbestad Gylterud (Apr 2020 – Nov 2023), Anders Mörtberg (Dec 2023 – Nov 2024).

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.