Hej!

I’m a recently graduated Ph.D. student in the computational mathematics division of the department of mathematics at Stockholm University. Here, I’ve been working on a project on homotopy type theory under the supervision of Anders Mörtberg. Soon, I’ll be starting a postdoc funded by a scholarship I was awarded by the Knut and Alice Wallenberg foundation with Ulrik Buchholtz at the School of Computer Science at the University of Nottingham.

My primary research interests are synethetic homotopy theory and computer formalisation, primarily in Cubical Agda. My thesis was mainly concerned the formalisation of cohomology theories and Guillaume Brunerie’s Ph.D. thesis. I’m interested in anything HoTT related. If you are too and would like to work on something together, please get in touch!

Current projects

Cellular (co)homology (joint with Anders Mörtberg and Loïc Pujet)

Cellular cohomology was developed by Buchholtz and Favonia in 2018. We are investigating whether their constructions can be used to develop (co)homology in a way that does not rely on previously defined cohomology theories. Thus far we have proved a version of the cellular approximation theorem and, using this, defined a homology functor. We are currently verifying that it satisfies the Eilenberg-Steenrod axioms.

Whitehead products in HoTT

Whitehead products were extensively used in Guillaume Brunerie’s Ph.D. thesis but few of their algebraic properties (e.g. bilinearity, graded commutativity, etc.) have been verified in HoTT. I’m currently working on verifying these, both in pen-and-paper HoTT and in Cubical Agda.

The fifth homotopy group of the 3-sphere in HoTT (joint with Tom Jack)

See here for an outline of the project.