| Title:
|
The Cayley-Dickson Construction in Homotopy Type Theory (English) |
| Author:
|
Buchholtz, Ulrik |
| Author:
|
Rijke, Egbert |
| Language:
|
English |
| Journal:
|
Higher Structures |
| ISSN:
|
2209-0606 |
| Volume:
|
2 |
| Issue:
|
1 |
| Year:
|
2018 |
| Pages:
|
30-41 |
| Summary lang:
|
English |
| . |
| Category:
|
math |
| . |
| Summary:
|
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. (English) |
| Keyword:
|
Homotopy Type Theory |
| MSC:
|
03B15 |
| MSC:
|
17A35 |
| MSC:
|
55P45 |
| MSC:
|
55U35 |
| idZBL:
|
Zbl 1522.03039 |
| idMR:
|
MR3917425 |
| DOI:
|
10.21136/HS.2018.02 |
| . |
| Date available:
|
2026-03-10T14:46:51Z |
| Last updated:
|
2026-03-10 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/153401 |
| . |
| Reference:
|
[1] Awodey, Steve, Warren, Michael A.: Homotopy theoretic models of identity types.Math. Proc. Cambridge Philos. Soc., Vol. 146, Iss. 1, 45-55, DOI:10.1017/S0305004108001783 10.1017/S0305004108001783 |
| Reference:
|
[2] Baez, John C.: The octonions.Bull. Amer. Math. Soc. (N.S.), Vol. 39, Iss. 2, 145-205, DOI:10.1090/S0273-0979-01-00934-X 10.1090/S0273-0979-01-00934-X |
| Reference:
|
[3] Berg, Benno, Garner, Richard: Topological and simplicial models of identity types.ACM Trans. Comput. Log., Vol. 13, Iss. 1, Art. 3, 44, DOI:10.1145/2071368.2071371 10.1145/2071368.2071371 |
| Reference:
|
[4] Bezem, Marc, Coquand, Thierry, Huber, Simon: A model of type theory in cubical sets.19th International Conference on Types for Proofs and Programs, pages 107-128, LIPIcs. Leibniz int. Proc. inform. 26 |
| Reference:
|
[5] Buchholtz, Ulrik: H-space structures on non-sphere suspensions?.http://mathoverflow.net/q/235840, MathOverflow Question |
| Reference:
|
[6] Cohen, Cyril, Coquand, Thierry, Huber, Simon, Mörtberg, Anders: Cubical type theory: A constructive interpretation of the univalence axiom.21st International Conference on Types for Proofs and Programs (TYPES 2015), pages , LIPIcs. Leibniz int. Proc. inform. |
| Reference:
|
[7] Dickson, Leonard E.: On quaternions and their generalization and the history of the eight square theorem.Ann. of Math. (2), Vol. 20, Iss. 3, 155-171, DOI:10.2307/1967865 10.2307/1967865 |
| Reference:
|
[8] Kapulkin, Chris, Lumsdaine, Peter LeFanu: The simplicial model of univalent foundations (after Voevodsky). |
| Reference:
|
[9] Licata, Daniel R., Brunerie, Guillaume: A cubical approach to synthetic homotopy theory.Proceedings of the 2015 30th annual ACM/IEEE symposium on logic in computer science (LICS), pp 92-103, DOI:10.1109/LICS.2015.19 10.1109/LICS.2015.19 |
| Reference:
|
[10] Martin-Löf, Per: Intuitionistic type theory.Studies in proof theory, Bibliopolis, ISBN:88-7088-105-9 |
| Reference:
|
[11] Moura, Leonardo, Kong, Soonho, Avigad, Jeremy, Doorn, Floris, Raumer, Jakob: The lean theorem prover (system description).Automated deduction – CADE-25, pp 378-388, DOI:10.1007/978-3-319-21401-6_26 10.1007/978-3-319-21401-6_26 |
| Reference:
|
[12] Rezk, Charles: Proof of the Blakers-Massey theorem.http://www.math.uiuc.edu/~rezk/freudenthal-and-blakers-
massey.pdf, Note |
| Reference:
|
[13] Serre, Jean-Pierre: Homologie singulière des espaces fibrés. Applications.Ann. of Math. (2), Vol. 54, 425-505 |
| Reference:
|
[14] Shulman, Michael: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory.Preprint |
| Reference:
|
[15] Shulman, Michael: The univalence axiom for elegant Reedy presheaves.Preprint |
| Reference:
|
[16] Shulman, Michael: Univalence for inverse EI diagrams.Homology, Homotopy and Applications, Vol. 19, Iss. 2, 219-249, DOI:10.4310/HHA.2017.v19.n2.a12 10.4310/HHA.2017.v19.n2.a12 |
| Reference:
|
[17] Univalent Foundations Program, The: Homotopy type theory: Univalent foundations of mathematics.http://homotopytypetheory.org/book/ |
| Reference:
|
[18] West, Robert W.: H-spaces which are co-H-spaces.Proc. Amer. Math. Soc., Vol. 31, 580-582 |
| . |
