Synthetic Integral Cohomology in Cubical Agda. - Guillaume Brunerie; Axel Ljungström; Anders Mörtberg (CSL, 2022)

Computing Cohomology Rings in Cubical Agda. - Thomas Lamiaux; Axel Ljungström; Anders Mörtberg (CPP, 2023)

Formalizing π4(S3) ≅Z/2Z and Computing a Brunerie Number in Cubical Agda. - Axel Ljungström; Anders Mörtberg (LICS, 2023)

Formalizing π4(S^3) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda. - Axel Ljungström; Anders Mörtberg (CoRR, 2023)

Computational Synthetic Cohomology Theory in Homotopy Type Theory. - Axel Ljungström; Anders Mörtberg (CoRR, 2024)

Formalising inductive and coinductive containers. - Stefania Damato; Thorsten Altenkirch; Axel Ljungström (CoRR, 2024)

Symmetric monoidal smash products in homotopy type theory. - Axel Ljungström (Math. Struct. Comput. Sci., 2024)

The Steenrod squares via unordered joins. - Axel Ljungström; David Wärn (CoRR, 2025)