The Cayley-Dickson Construction in Homotopy Type Theory

TL;DR

This paper constructs an H-space structure on the 3-sphere within homotopy type theory, providing a homotopy-invariant description of the quaternionic Hopf fibration without relying on classical topology tools.

Contribution

It introduces a novel homotopy type theory approach to model the quaternionic Hopf fibration and H-space structure on -sphere, advancing the intersection of type theory and algebraic topology.

Findings

H-space structure on -sphere established in homotopy type theory

Homotopy-invariant description of the quaternionic Hopf fibration

New methods for modeling classical topological constructs in type theory

Abstract

We define in the setting of homotopy type theory an H-space structure on $\mathbb S^3$. Hence we obtain a description of the quaternionic Hopf fibration $\mathbb S^3\hookrightarrow\mathbb S^7\twoheadrightarrow\mathbb S^4$, using only homotopy invariant tools.