The James construction and _4(S^3) in homotopy type theory

DOI10.1007/S10817-018-9468-2MaRDI QIDQ2319987zbMATH OpenOpenAlexFDO

Authors Guillaume Brunerie

Publication date 21 August 2019

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1710.10307

zbMATH Keywords

homotopy type theoryhomotopy groups of spheresJames construction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Abstract: In the first part of this paper we present a formalization in Agda of the James construction in homotopy type theory. We include several fragments of code to show what the Agda code looks like, and we explain several techniques that we used in the formalization. In the second part, we use the James construction to give a constructive proof that $p{i}_4(mathbb{S}^3)$ is of the form $mathbbZ/nmathbbZ$ (but we do not compute the $n$ here).

Recommendations

• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• \(\pi _{n }(S ^{n })\) in homotopy type theory
• The Cayley-Dickson construction in homotopy type theory
• Eilenberg-MacLane spaces in homotopy type theory
• Cellular Cohomology in Homotopy Type Theory

Cites work

• A cubical approach to synthetic homotopy theory
• A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory
• Homotopy type theory. Univalent foundations of mathematics

Cited in

(6)

• An introduction to univalent foundations for mathematicians
• On the James and Hilton-Milnor splittings, and the metastable EHP sequence
• A type theory for strictly unital \(\infty \)-categories
• Semantics for two-dimensional type theory
• Syllepsis in homotopy type theory
• The Cayley-Dickson construction in homotopy type theory

Describes a project that uses

Uses Software

• Agda

This page was built for publication: The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2319987)