Formalising inductive and coinductive containers
Submitted
Stefania Damato, Thorsten Altenkirch, Axel Ljungström
Arxiv
Publications and preprints
Computational Synthetic Cohomology Theory in Homotopy Type Theory
Submitted, 2024
Axel Ljungström, Anders Mörtberg
Arxiv
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)
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’
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)
Computing Cohomology Rings in Cubical Agda
Proceedings of CPP 2023
Thomas Lamiaux, Axel Ljungström, Anders Mörtberg
Arxiv
Distinguished paper award (CPP 2023)
Synethetic Integral Cohomology in Cubical Agda
Proceedings of CSL 2022
Guillaume Brunerie, Axel Ljungström, Anders Mörtberg
Available here