Synethetic Integral Cohomology in Cubical Agda
Guillaume Brunerie, Axel Ljungström, Anders Mörtberg, Proceedings of CSL 2022
CV
Education
- B.S. in Theoretical Philosophy, Stockholm University, 2018
- B.S. in Mathematics, Stockholm University, 2018
- M.S. in Mathematics, Stockholm University, 2020
- Ph.D in Computational Mathematics, Stockholm University, 2025
Work experience
- 2019-2020 : Teaching assistant (amanuens)
- Stockholm University, Department of Mathematics
- Duties included: Tutoring, grading (mathematics courses)
- Summer 2018: Digitaliser and mathematics educator
- Liber
- Duties included: Digitalisation of high-school level maths textbooks and solution writing
Publications
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux, Axel Ljungström, Anders Mörtberg, Proceedings of CPP 2023
Formalizing π₄(S³) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda
Axel Ljungström, Anders Mörtberg, Proceedings of LICS 2023
Formalising and Computing the Fourth Homotopy Group of the 3-Sphere in Cubical Agda
Axel Ljungström, Anders Mörtberg, Submitted, 2023
Symmetric Monoidal Smash Products in Homotopy Type Theory
Axel Ljungström, Mathematical Structures in Computer Science, 2024
Cellular Methods in Homotopy Type Theory
Axel Ljungström, Loïc Pujet, Preprint, 2025
The Steenrod squares via unordered joins
Axel Ljungström, David Wärn, To appear in Proceedings of LICS 2025
Formalising inductive and coinductive containers
Stefania Damato, Thorsten Altenkirch, Axel Ljungström, To appear at ITP 2025
Computational Synthetic Cohomology Theory in Homotopy Type Theory
Axel Ljungström, Anders Mörtberg, Mathematical Structures in Computer Science, 2025
Talks
Cohomology Computations in Cubical Agda
Talk at Stockholm–Göteborg joint type theory seminar, Online
Synthetic Integral Cohomology in Cubical Agda
Talk at CSL 2022, Online
Cohomology Theory and Brunerie Numbers in Cubical Agda
Talk at Formalization of Cohomology Theories, Banff, Canada/Online
The 4th Homotopy Group of the 3-Sphere in Cubical Agda
Talk at TYPES 2022, Nantes, France
Formalizing π₄(S³) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda
Talk at LICS 2023, Boston, USA/Online
Calculating a Brunerie Number
Talk at Homotopy Type Theory Electronic Seminar Talks, Online
Dealing With Smash Products in HoTT
Talk at Stockholm–Göteborg joint type theory seminar, Gothenburg, Sweden
Smash Products Are Symmetric Monoidal in HoTT
Talk at HoTT/UF 2023, Vienna, Austria
Introduction to Cubical Agda
Talk at Seminar (Logical Foundations of Computation), University of Turin, Turin, Italy
π₄(S³) ≅ ℤ/2ℤ Cubical Agda
Talk at Seminar (Logical Foundations of Computation), University of Turin, Turin, Italy
Symmetric Monoidal Smash Products in HoTT
Talk at The Second International Conference on Homotopy Type Theory (HoTT 2023), Pittsburgh, USA
Cellular Homology and the Cellular Approximation Theorem
Talk at HoTT/UF 2024, Leuven, Belgium
The Steenrod Squares in HoTT Revisited
Talk at HoTT/UF 2024, Leuven, Belgium
Revisiting the Steenrod Squares in HoTT
Talk at TYPES 2024, Copenhagen, Denmark
Some properties of Whitehead products
Talk at HoTT/UF 2025, Genoa, Italy
Yet another homotopy group, yet another Brunerie number
Talk at TYPES 2025, Glasgow, Scotland
Teaching
Teaching assistant (mathematics)
Stockholm University, Department of Mathematics
Teaching assistant (computational mathematics)
Stockholm University, Department of Mathematics
HoTTEST Summer School 2022
Online