arXiv subjects

Axel Ljungström

Publications and source records attributed to Axel Ljungström.

7 recordsLinked to original sources

arXiv2026

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can be composed. We show that all higher coherences can be stated and derived if simplicial type theory is taken to be homotopy type theory with a postulated interval type. In technical terms, this means that if a type has unique fillers for $(2,1)$-horns, it has unique fillers for all inner $(n,k)$-horns. This generalizes a result of Riehl and Shulman for the case $n = 3, k \in \{1, 2\}$. Our main technical tool is the Leibniz adjunction: the pushout-product is left adjoint to the pullback-hom in the wild category of types. While this adjunction is well known for ordinary categories, it is much more involved for higher categories, and the fact that it can be proved for the wild category of types (a higher category without stated higher coherences) is non-trivial. We make profitable use of the equivalence between the wild category of maps and that of families. We have formalized the results in Cubical Agda.

math.CT↗

arXiv2025

Formalising Inductive and Coinductive Containers

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.

cs.LO↗

arXiv2025

The Steenrod squares via unordered joins

The Steenrod squares are cohomology operations with important applications in algebraic topology. While these operations are well-understood classically, little is known about them in the setting of homotopy type theory. Although a definition of the Steenrod squares was put forward by Brunerie (2017), proofs of their characterising properties have remained elusive. In this paper, we revisit Brunerie's definition and provide proofs of these properties, including stability, Cartan's formula and the Adem relations. This is done by studying a higher inductive type called the unordered join. This approach is inherently synthetic and, consequently, many of our proofs differ significantly from their classical counterparts. Along the way, we discuss upshots and limitations of homotopy type theory as a synthetic language for homotopy theory. The paper is accompanied by a computer formalisation in Cubical Agda.

math.AT↗

arXiv2024

Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda

Brunerie's 2016 PhD thesis contains the first synthetic proof in Homotopy Type Theory (HoTT) of the classical result that the fourth homotopy group of the 3-sphere is $\mathbb{Z}/2\mathbb{Z}$. The proof is one of the most impressive pieces of synthetic homotopy theory to date and uses a lot of advanced classical algebraic topology rephrased synthetically. Furthermore, the proof is fully constructive and the main result can be reduced to the question of whether a particular "Brunerie number" $β$ can be normalised to $\pm 2$. The question of whether Brunerie's proof could be formalised in a proof assistant, either by computing this number or by formalising the pen-and-paper proof, has since remained open. In this paper, we present a complete formalisation in Cubical Agda. We do this by modifying Brunerie's proof so that a key technical result, whose proof Brunerie only sketched in his thesis, can be avoided. We also present a formalisation of a new and much simpler proof that $β$ is $\pm 2$. This formalisation provides us with a sequence of simpler Brunerie numbers, one of which normalises very quickly to $-2$ in Cubical Agda, resulting in a fully formalised computer-assisted proof that $π_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$.

math.AT↗

arXiv2024

Computational Synthetic Cohomology Theory in Homotopy Type Theory

This paper discusses the development of synthetic cohomology in Homotopy Type Theory (HoTT), as well as its computer formalisation. The objectives of this paper are (1) to generalise previous work on integral cohomology in HoTT by the current authors and Brunerie (2022) to cohomology with arbitrary coefficients and (2) to provide the mathematical details of, as well as extend, results underpinning the computer formalisation of cohomology rings by the current authors and Lamiaux (2023). With respect to objective (1), we provide new direct definitions of the cohomology group operations and of the cup product, which, just as in (Brunerie et al., 2022), enable significant simplifications of many earlier proofs in synthetic cohomology theory. In particular, the new definition of the cup product allows us to give the first complete formalisation of the axioms needed to turn the cohomology groups into a graded commutative ring. We also establish that this cohomology theory satisfies the HoTT formulation of the Eilenberg-Steenrod axioms for cohomology and study the classical Mayer-Vietoris and Gysin sequences. With respect to objective (2), we characterise the cohomology groups and rings of various spaces, including the spheres, torus, Klein bottle, real/complex projective planes, and infinite real projective space. All results have been formalised in Cubical Agda and we obtain multiple new numbers, similar to the famous `Brunerie number', which can be used as benchmarks for computational implementations of HoTT. Some of these numbers are infeasible to compute in Cubical Agda and hence provide new computational challenges and open problems which are much easier to define than the original Brunerie number.

math.AT↗

arXiv2024

Symmetric Monoidal Smash Products in Homotopy Type Theory

In Homotopy Type Theory, few constructions have proved as troublesome as the smash product. While its definition is just as direct as in classical mathematics, one quickly realises that in order to define and reason about functions over iterations of it, one has to verify an exponentially growing number of coherences. This has led to crucial results concerning smash products remaining open. One particularly important such result is the fact that smash products form a (1-coherent) symmetric monoidal product on the universe of pointed types. This fact was used, without a complete proof, by e.g. Brunerie in his PhD thesis to construct the cup product on integral cohomology and is, more generally, a fundamental result in traditional algebraic topology. In this paper, we salvage the situation by introducing a simple informal heuristic for reasoning about functions defined over iterated smash products. We then use the heuristic to verify e.g. the hexagon and pentagon identities, thereby obtaining a proof of symmetric monoidality. We also provide a formal statement of the heuristic in terms of an induction principle concerning the construction of homotopies of functions defined over iterated smash products. The key results presented here have been formalised in the proof assistant Cubical Agda.

math.AT↗

arXiv2022

Computing Cohomology Rings in Cubical Agda

In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first fully mechanized definition of cohomology rings. These rings may be defined as direct sums of cohomology groups together with a multiplication induced by the cup product, and can in many cases be characterized as quotients of multivariate polynomial rings. To this end, we introduce appropriate definitions of direct sums and graded rings, which we then use to define both cohomology rings and multivariate polynomial rings. Using this, we compute the cohomology rings of some classical spaces, such as the spheres and the Klein bottle. The formalization is constructive so that it can be used to do concrete computations, and it relies on the Cubical Agda system which natively supports higher inductive types and computational univalence.

math.AT↗