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

DOI10.1007/S10817-018-9468-2zbMATH Open1477.03035arXiv1710.10307OpenAlexW2963650711MaRDI QIDQ2319987FDOQ2319987

Authors: Guillaume Brunerie 

Publication date: 21 August 2019

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

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).

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

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

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)

Cites Work

• Homotopy type theory. Univalent foundations of mathematics
• A Cubical Approach to Synthetic Homotopy Theory
• A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

Cited In (6)

• On the James and Hilton-Milnor splittings, and the metastable EHP sequence
• Formalization of the fundamental group in untyped set theory using auto2
• A type theory for strictly unital \(\infty \)-categories
• Semantics for two-dimensional type theory
• Syllepsis in homotopy type theory
• An introduction to univalent foundations for mathematicians

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)