Computing Cohomology Rings in Cubical Agda
Published:
Thomas Lamiaux, Axel Ljungström, Anders Mörtberg
Available here
Distinguished paper award
Posts by Collection
misc
Formalizing π₄(S³) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda
Published:
Download here
portfolio
Portfolio item number 1
Short description of portfolio item number 1
Portfolio item number 2
Short description of portfolio item number 2
publications
Synethetic Integral Cohomology in Cubical Agda
Proceedings of CSL 2022
Guillaume Brunerie, Axel Ljungström, Anders Mörtberg
Available here
Computing Cohomology Rings in Cubical Agda
Proceedings of CPP 2023
Thomas Lamiaux, Axel Ljungström, Anders Mörtberg
Arxiv
Distinguished Paper Award (CPP 2023)
Formalizing π₄(S³) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda
Proceedings of LICS 2023
Axel Ljungström, Anders Mörtberg
Arxiv
Distinguished Paper Award (LICS 2023)
Formalising and Computing the Fourth Homotopy Group of the 3-Sphere in Cubical Agda
Submitted, 2023
Axel Ljungström, Anders Mörtberg
Arxiv
Extended version of `Formalizing π₄(S³) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda’
Symmetric Monoidal Smash Products in Homotopy Type Theory
Mathematical Structures in Computer Science, 2024
Axel Ljungström
Available here
Preprint version awarded best student paper (HoTT 2023)
Cellular Methods in Homotopy Type Theory
Preprint, 2025
Axel Ljungström, Loïc Pujet
Available here
The Steenrod squares via unordered joins
To appear in Proceedings of LICS 2025
Axel Ljungström, David Wärn
Arxiv
Distinguished Paper Award (LICS 2025)
Kleene Award (LICS 2025)
Formalising inductive and coinductive containers
To appear at ITP 2025
Stefania Damato, Thorsten Altenkirch, Axel Ljungström
Arxiv
Computational Synthetic Cohomology Theory in Homotopy Type Theory
Mathematical Structures in Computer Science, 2025
Axel Ljungström, Anders Mörtberg
Available here
talks
Cohomology Computations in Cubical Agda
Published:
Calculating a Brunerie Number
Published:
Dealing With Smash Products in HoTT
Published:
Introduction to Cubical Agda
Published:
π₄(S³) ≅ ℤ/2ℤ Cubical Agda
Published:
Symmetric Monoidal Smash Products in HoTT
Published:
The Steenrod Squares in HoTT Revisited
Published:
Revisiting the Steenrod Squares in HoTT
Published:
Some properties of Whitehead products
Published:
teaching
Teaching assistant (mathematics)
Undergraduate courses in mathematics, Stockholm University, Department of Mathematics, 2019
Teaching assistant for various courses in mathematics taught between 2019 and 2020. Duties primarily included tutoring and grading. See the following list for the courses I have been part of.
Teaching assistant (computational mathematics)
Undergraduate courses in computational mathematics, Stockholm University, Department of Mathematics, 2020
Teaching assistant for various courses in computational mathematics, starting 2020 (ongoing). Duties primarily include exercise sessions, tutoring and grading. See the following list for the courses I am/have been part of.
HoTTEST Summer School 2022
Summer school, Online, 2022
Summer school on homotopy type theory and Agda. I was a teaching assistant involved in tutoring and holding exercise sessions. All lectures and exercise sessions can be found here, including my sessions.