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. My research is about developing mathematics in homotopy type theory. I am also generally interested in 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).
• 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

• A project on verifying properties of Steenrod squares in HoTT, with Axel Ljungström
• Higher equivalence relations in homotopy type theory
• Various results in synthetic algebraic geometry (repository)
• Unordered addition from biproducts (draft)

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.