A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
2016 (English)In: LICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, New York, USA: Association for Computing Machinery (ACM), 2016Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
New York, USA: Association for Computing Machinery (ACM), 2016.
Algebra and Logic
Research subject Mathematical Logic
IdentifiersURN: urn:nbn:se:su:diva-140143DOI: 10.1145/2933575.2934545ISBN: 978-1-4503-4391-6 (print)OAI: oai:DiVA.org:su-140143DiVA: diva2:1077736
LICS 2016 — ACM/IEEE Symposium on Logic in Computer Science