Search Results

Documents authored by Ljungström, Axel

Artifact
Software
DOI: 10.4230/artifacts.26875
Cellular Methods in Homotopy Type Theory (accompanying formalisation)

Authors: Axel Ljungström and Loïc Pujet

Abstract
Cite as

Axel Ljungström, Loïc Pujet. Cellular Methods in Homotopy Type Theory (accompanying formalisation) (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26875,
   title = {{Cellular Methods in Homotopy Type Theory (accompanying formalisation)}}, 
   author = {Ljungstr\"{o}m, Axel and Pujet, Lo\"{i}c},
   note = {Software, Knut and Alice Wallenberg Foundation Postdoctoral Scholarship: Program in Mathematics for researchers with a Swedish doctor’s degree, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:7904cf81046d351ce2a27f778d8b96f71186035d;origin=https://github.com/agda/cubical;visit=swh:1:snp:82843e2d41d4b8b6a9013ffeadeb01fbcbb23e53;anchor=swh:1:rev:8a45d739ad0b75f4773874be4a5e42dbd46c9cd6}{\texttt{swh:1:dir:7904cf81046d351ce2a27f778d8b96f71186035d}} (visited on 2026-07-09)},
   url = {https://github.com/agda/cubical/blob/master/Cubical/Papers/CellularMethods.agda},
   doi = {10.4230/artifacts.26875},
}
Artifact
Software
DOI: 10.4230/artifacts.26876
A Computer Formalisation of the Serre Finiteness Theorem (accompanying formalisation)

Authors: Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg

Abstract
Cite as

Reid Barton, Axel Ljungström, Owen Milner, Anders Mörtberg. A Computer Formalisation of the Serre Finiteness Theorem (accompanying formalisation) (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{SerreFiniteness,
   title = {{A Computer Formalisation of the Serre Finiteness Theorem (accompanying formalisation)}}, 
   author = {Barton, Reid and Ljungstr\"{o}m, Axel and Milner, Owen and M\"{o}rtberg, Anders},
   note = {Software, ForCUTT project, ERC advanced grant 101053291, Knut & Alice Wallenberg Foundation’s Program for Mathematics, This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0009, PI Steve Awodey, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:5c9314da89014673a22878132bb63cfc42ccfa73;origin=https://github.com/CMU-HoTT/serre-finiteness;visit=swh:1:snp:0f3bfe0f67361dc33562f0fc15b80309b3290611;anchor=swh:1:rev:79f3150942a129eb544004adcdef4b17244d5ed4}{\texttt{swh:1:dir:5c9314da89014673a22878132bb63cfc42ccfa73}} (visited on 2026-07-09)},
   url = {https://github.com/CMU-HoTT/serre-finiteness},
   doi = {10.4230/artifacts.26876},
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.16
A Computer Formalisation of the Serre Finiteness Theorem

Authors: Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
Few constructions in mathematics are as elusive as the homotopy groups of spheres. These groups, which intuitively measure n-dimensional loops on m-dimensional spheres, appear at first glance to be almost completely random - an unfortunate fact, seeing as they constitute one of the fundamental building blocks of algebraic topology and homotopy theory. However, the situation is not completely hopeless: in 1951, Serre proved his celebrated finiteness theorem, which says that these groups are almost always finite abelian groups, except in two classes of special cases when they also contain copies of the integers. In a recent paper, Barton and Campion proved a variation of this result in homotopy type theory (HoTT) - an extension of Martin-Löf type theory, particularly suitable for reasoning about and formalising algebraic topology and homotopy theory. Their result shows that the homotopy groups of spheres are all finitely presented - and constructively so. Prior to this proof, only low-dimensional homotopy groups of spheres had been computed in HoTT. This made it a major breakthrough for HoTT as a foundation and, as such, the immediate target of a full-scale formalisation project. In this paper, we present the outcome of this project: a complete formalisation of Barton and Campion’s proof of the Serre finiteness theorem in Cubical Agda, a constructive proof assistant implementing a cubical flavour of HoTT. In the light of the constructivity of Cubical Agda, we discuss the prospect of running the algorithm provided by our formalisation in order to compute concrete homotopy groups of spheres.
Cite as

Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg. A Computer Formalisation of the Serre Finiteness Theorem. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 16:1-16:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{barton_et_al:LIPIcs.LICS.2026.16,
  author =	{Barton, Reid and Ljungstr\"{o}m, Axel and Milner, Owen and M\"{o}rtberg, Anders},
  title =	{{A Computer Formalisation of the Serre Finiteness Theorem}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{16:1--16:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.16},
  URN =		{urn:nbn:de:0030-drops-268031},
  doi =		{10.4230/LIPIcs.LICS.2026.16},
  annote =	{Keywords: Homotopy type theory, synthetic homotopy theory, formalisation of mathematics, constructive mathematics}
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.66
Cellular Methods in Homotopy Type Theory

Authors: Axel Ljungström and Loïc Pujet

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
In classical mathematics, a CW complex is a topological space which can be built up inductively by gluing together cells of increasing dimension. Thanks to their excellent categorical properties, CW complexes have become one of the main objects of interest in algebraic topology. Although their quasi-combinatorial nature suggests that a constructive treatment is possible, there seems to be little literature on the subject - perhaps because of the important role played by the axiom of choice in the classical theory of CW complexes. In this paper, we present a synthetic and constructive account of the theory of CW complexes in homotopy type theory. Our first main result is a finitary version of the cellular approximation theorem which, among other things, allows us to construct a cellular homology functor without needing the axiom of choice or relying on a pre-existing notion of homology. Our second main result, which we call the "Hurewicz approximation theorem", shows that the CW complexes that are n-connected types are precisely the ones that can be presented by a CW structure with no nontrivial cells up to dimension n. This theorem is standard in the classical treatment of CW complexes, but it is far from being obvious in a constructive setting. As a corollary, we give a new proof of the Hurewicz theorem for CW complexes, which relates the first non-vanishing homotopy group of a CW complex with the corresponding homology group. All key theorems presented in this paper have been mechanised in Cubical Agda.
Cite as

Axel Ljungström and Loïc Pujet. Cellular Methods in Homotopy Type Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 66:1-66:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ljungstrom_et_al:LIPIcs.LICS.2026.66,
  author =	{Ljungstr\"{o}m, Axel and Pujet, Lo\"{i}c},
  title =	{{Cellular Methods in Homotopy Type Theory}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{66:1--66:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.66},
  URN =		{urn:nbn:de:0030-drops-268536},
  doi =		{10.4230/LIPIcs.LICS.2026.66},
  annote =	{Keywords: Homotopy type theory, Univalent foundations, constructive mathematics, synthetic homotopy theory, CW complexes, cellular homology, Hurewicz theorem}
}
Artifact
Software
DOI: 10.4230/artifacts.24710
stefaniatadama/formalising-inductive-coinductive-containers

Authors: Stefania Damato, Thorsten Altenkirch, and Axel Ljungström

Abstract
Cite as

Stefania Damato, Thorsten Altenkirch, Axel Ljungström. stefaniatadama/formalising-inductive-coinductive-containers (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24710,
   title = {{stefaniatadama/formalising-inductive-coinductive-containers}}, 
   author = {Damato, Stefania and Altenkirch, Thorsten and Ljungstr\"{o}m, Axel},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:a75b7ddaa46ca9a9f3ee6f65d22ba3b1c959d6d4;origin=https://github.com/stefaniatadama/formalising-inductive-coinductive-containers;visit=swh:1:snp:eebf2acbd002c4877bc6057e65e8ddef2b0fe79e;anchor=swh:1:rev:4e587677bdc0c7cb793ad8612c1e6e88c16877e7}{\texttt{swh:1:dir:a75b7ddaa46ca9a9f3ee6f65d22ba3b1c959d6d4}} (visited on 2025-09-22)},
   url = {https://github.com/stefaniatadama/formalising-inductive-coinductive-containers/blob/main/cubical/Cubical/Papers/Containers.agda},
   doi = {10.4230/artifacts.24710},
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.17
Formalising Inductive and Coinductive Containers

Authors: Stefania Damato, Thorsten Altenkirch, and Axel Ljungström

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of locally cartesian closed categories (LCCCs) with disjoint coproducts and W-types, and uniqueness of identity proofs (UIP) is implicitly assumed throughout. Although it is claimed that these developments can also be interpreted in extensional Martin-Löf type theory, this interpretation is not made explicit. In this paper, we present a formalisation of the results that "containers preserve least and greatest fixed points" in Cubical Agda, thereby giving a formulation in intensional type theory. Our proofs do not make use of UIP and thereby generalise the original results from talking about container functors on Set to container functors on the wild category of types. Our main incentive for using Cubical Agda is that its path type restores the equivalence between bisimulation and coinductive equality. Thus, besides developing container theory in a more general setting, we also demonstrate the usefulness of Cubical Agda’s path type to coinductive proofs.
Cite as

Stefania Damato, Thorsten Altenkirch, and Axel Ljungström. Formalising Inductive and Coinductive Containers. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{damato_et_al:LIPIcs.ITP.2025.17,
  author =	{Damato, Stefania and Altenkirch, Thorsten and Ljungstr\"{o}m, Axel},
  title =	{{Formalising Inductive and Coinductive Containers}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.17},
  URN =		{urn:nbn:de:0030-drops-246151},
  doi =		{10.4230/LIPIcs.ITP.2025.17},
  annote =	{Keywords: type theory, container, initial algebra, terminal coalgebra, Cubical Agda}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.11
Synthetic Integral Cohomology in Cubical Agda

Authors: Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
This paper discusses the formalization of synthetic cohomology theory in a cubical extension of Agda which natively supports univalence and higher inductive types. This enables significant simplifications of many proofs from Homotopy Type Theory and Univalent Foundations as steps that used to require long calculations now hold simply by computation. To this end, we give a new definition of the group structure for cohomology with ℤ-coefficients, optimized for efficient computations. We also invent an optimized definition of the cup product which allows us to give the first complete formalization of the axioms needed to turn the integral cohomology groups into a graded commutative ring. Using this, we characterize the cohomology groups of the spheres, torus, Klein bottle and real/complex projective planes. As all proofs are constructive we can then use Cubical Agda to distinguish between spaces by computation.
Cite as

Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg. Synthetic Integral Cohomology in Cubical Agda. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{brunerie_et_al:LIPIcs.CSL.2022.11,
  author =	{Brunerie, Guillaume and Ljungstr\"{o}m, Axel and M\"{o}rtberg, Anders},
  title =	{{Synthetic Integral Cohomology in Cubical Agda}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.11},
  URN =		{urn:nbn:de:0030-drops-157310},
  doi =		{10.4230/LIPIcs.CSL.2022.11},
  annote =	{Keywords: Synthetic Homotopy Theory, Cohomology Theory, Cubical Agda}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact