David Wärn

email: warnd@chalmers.se

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 particularly interested in synthetic higher category theory. I am also generally interested in constructive mathematics and proof assistants. I started my PhD in 2021, and before that I studied pure mathematics at Trinity College, Cambridge (BA+MMath).

Click here to see a picture of me.

Papers and preprints

• A synthetic construction of universal cocartesian fibrations, with Christian Sattler
• 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.

In preparation (as of April 2026)

• Higher equivalence relations in homotopy type theory
• Some extensions and applications of the zigzag construction

Abandoned drafts

• Unordered addition from biproducts

Older work

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.