Higher Structures, Vol. 2, No. 1, pp. 30-41, 2018

The Cayley-Dickson Construction in Homotopy Type Theory

Egbert Rijke, Ulrik Buchholtz

Received October 25th 2016. Published online November 8th 2018.

Abstract:  We define in the setting of homotopy type theory an H-space structure on $\Bbb S^3$. Hence we obtain a description of the quaternionic Hopf fibration $\Bbb S^3 \hookrightarrow \Bbb S^7 \twoheadrightarrow \Bbb S^4 $, using only homotopy invariant tools. A side benefit is that the construction applies to more general $\infty$-categories than that of spaces.
Keywords:  Homotopy Type Theory
Classification MSC:  03B15, 17A35, 55P45, 55U35

PDF available at:  Institute of Mathematics CAS

Affiliations:   Egbert Rijke, Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA 15213, USA, e-mail: erijke@andrew.cmu.edu; Ulrik Buchholtz, Current address: Fachbereich Mathematik, Technische Universität Darmstadt, Schlossgartenstraße 7, 64289 Darmstadt, Germany, e-mail: buchholtz@mathematik.tu-darmstadt.de

PDF available at: