A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory

DOI10.1145/2933575.2934545MaRDI QIDQ4635917zbMATH OpenOpenAlexFDO

Authors Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, Peter Lefanu Lumsdaine

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Loop spaces (55P35) Suspensions (55P40) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Abstract: This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present a mechanized proof of the Blakers-Massey connectivity theorem, a result relating the higher-dimensional homotopy groups of a pushout type (roughly, a space constructed by gluing two spaces along a shared subspace) to those of the components of the pushout. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which has been studied in previous formalizations. The new proof is more elementary than existing ones in abstract homotopy-theoretic settings, and the mechanization is concise and high-level, thanks to novel combinations of ideas from homotopy theory and type theory.

Recommendations

• The Seifert-van Kampen Theorem in Homotopy Type Theory
• A generalized Blakers–Massey theorem
• A purely homotopy-theoretic proof of the Blakers-Massey theorem for n-cubes
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Eilenberg-MacLane spaces in homotopy type theory

Cited in

(19)

• The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
• Internal languages of finitely complete ( , 1)-categories
• Eilenberg-MacLane spaces in homotopy type theory
• An introduction to univalent foundations for mathematicians
• Cellular cohomology in homotopy type theory
• A generalized Blakers–Massey theorem
• Modalities in homotopy type theory
• The Hurewicz theorem in homotopy type theory
• Strange new universes: Proof assistants and synthetic foundations
• Topological quantum gates in homotopy type theory
• Homotopy type theory as a language for diagrams of -logoses
• Covering spaces in homotopy type theory
• Classification of covering spaces and canonical change of basepoint
• Automating boundary filling in cubical Agda
• Toward a geometry for syntax
• Computational synthetic cohomology theory in homotopy type theory
• On symmetries of spheres in univalent foundations
• Coslice colimits in homotopy type theory
• Automating boundary filling in cubical type theories

This page was built for publication: A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory

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