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 (expected)
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
Symmetric Monoidal Smash Products in Homotopy Type Theory
Axel Ljungström, To appear in Mathematical Structures in Computer Science
Computational Synthetic Cohomology Theory in Homotopy Type Theory
Axel Ljungström, Anders Mörtberg, Submitted, 2024
Formalising inductive and coinductive containers
Stefania Damato, Thorsten Altenkirch, Axel Ljungström, Submitted
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
Teaching
Teaching assistant (mathematics)
Stockholm University, Department of Mathematics
Teaching assistant (computational mathematics)
Stockholm University, Department of Mathematics
HoTTEST Summer School 2022
Online