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. I am looking for a postdoc position starting in 2027. 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.

Axioms for higher category theory

With Christian Sattler, I have been thinking about how to extend homotopy type theory with axioms that allow a development of higher category theory. You can read about it from these slides, or from this forest (last updated in November 2025).

In preparation (as of May 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.