On symmetries of spheres in univalent foundations
Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus, Marc Bezem
TL;DR
The paper develops a synthetic homotopy-theoretic account of sphere symmetries in univalent foundations, proving that for $n\ge2$ the type $({\mathbb S^{n}}={\mathbb S^{n}})$ has exactly two connected components, each with fundamental group $\mathbb{Z}/2\mathbb{Z}$. It first resolves the circle case via Gottlieb-type univalent group theory, then establishes a two-component structure for $\mathbb S^{2}$ using the Hopf fibration and degree theory, and finally extends to all $n$ by induction using suspension and the wild adjunction $\Sigma\dashv \Omega$. The work introduces and exploits a pair of degree maps, analyzes Whitehead products via a live EHP-type framework, and provides concrete symmetry representatives, while drawing connections to classical topology and sphere-spectrum units. Overall, the results illuminate how univalence and higher inductive types yield a coherent two-component picture of sphere symmetries and open avenues toward deeper connections with classical invariants and spectral data in UF.
Abstract
Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form $\mathbb{S}^n = \mathbb{S}^n$. The case of the circle has a slick answer: the symmetries of the circle form two copies of the circle. For higher-dimensional spheres, the type of symmetries has again two connected components, namely the components of the maps of degree plus or minus one. Each of the two components has $\mathbb{Z}/2\mathbb{Z}$ as fundamental group. For the latter result, we develop an EHP long exact sequence.