Article
Full entry |
PDF
(0.6 MB)
Feedback
PDF
(0.6 MB)
Feedback
Keywords:
Homotopy Type Theory
Homotopy Type Theory
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.
References:
[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 DOI 10.1017/S0305004108001783
[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 DOI 10.1090/S0273-0979-01-00934-X
[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 DOI 10.1145/2071368.2071371
[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
[5] Buchholtz, Ulrik: H-space structures on non-sphere suspensions?. http://mathoverflow.net/q/235840, MathOverflow Question
[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.
[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 DOI 10.2307/1967865
[8] Kapulkin, Chris, Lumsdaine, Peter LeFanu: The simplicial model of univalent foundations (after Voevodsky).
[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 DOI 10.1109/LICS.2015.19
[10] Martin-Löf, Per: Intuitionistic type theory. Studies in proof theory, Bibliopolis, ISBN:88-7088-105-9
[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 DOI 10.1007/978-3-319-21401-6_26
[12] Rezk, Charles: Proof of the Blakers-Massey theorem. http://www.math.uiuc.edu/~rezk/freudenthal-and-blakers-
massey.pdf, Note
[13] Serre, Jean-Pierre: Homologie singulière des espaces fibrés. Applications. Ann. of Math. (2), Vol. 54, 425-505
[14] Shulman, Michael: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Preprint
[15] Shulman, Michael: The univalence axiom for elegant Reedy presheaves. Preprint
[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 DOI 10.4310/HHA.2017.v19.n2.a12
[17] Univalent Foundations Program, The: Homotopy type theory: Univalent foundations of mathematics. http://homotopytypetheory.org/book/
[18] West, Robert W.: H-spaces which are co-H-spaces. Proc. Amer. Math. Soc., Vol. 31, 580-582
Search
Partner of
