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
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
To appear in Mathematical Structures in Computer Science
Axel Ljungström
Arxiv
First version awarded best student paper (HoTT 2023)
Computational Synthetic Cohomology Theory in Homotopy Type Theory
Submitted, 2024
Axel Ljungström, Anders Mörtberg
Arxiv
Formalising inductive and coinductive containers
Submitted
Stefania Damato, Thorsten Altenkirch, Axel Ljungström
Arxiv
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:
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.