David Wärn

I am a PhD student in the Department of Computer Science and Engineering at the University of Gothenburg, supervised by Thierry Coquand and Christian Sattler, expecting to graduate in 2026. My research is about developing mathematics in homotopy type theory. I am also generally interested in higher category theory, constructive mathematics, proof assistants, and homotopy theory. I started my PhD in 2021, and before that I studied pure mathematics at Trinity College, Cambridge (BA+MMath).

Papers and preprints

Path spaces of pushouts. A recording from a HoTTEST talk is available here (slides). An older, more explicitly type-theoretic version remains available (here).
The Steenrod squares via unordered joins, with Axel Ljungström, presented at LICS'25.
Confluent colimits commute with pullbacks, given descent (draft), with Christian Sattler.
On internally projective sheaves of groups
Natural numbers from integers (formalisation), with Christian Sattler, presented at LICS 2024.
Eilenberg–MacLane spaces and stabilisation in homotopy type theory, published in Journal of Homotopy and Related Structures.

I have made some contributions to Lean's library of formalised mathematics, mostly before the start of my PhD:

In Ramsey theory I proved the Hales-Jewett theorem, Hindman's theorem on finite sums, and Deuber's theorem on the partition regularity of (m,p,c)-sets.
In group theory I proved the Nielsen-Schreier theorem, which says that no group can be free until all its subgroups are free, and constructed free products.
In order theory / logic I proved the Rasiowa–Sikorski lemma and used it to show that any two countable dense linear orders are isomorphic

Partinioning permutations into monotone subsequences: the result of a 2020 summer research project in combinatorics, supervised by Imre Leader.