Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
Stockholm University, Faculty of Science, Department of Mathematics.ORCID iD: 0000-0003-1390-2970
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), 2016, 565-574 p.Conference paper, (Refereed)
Abstract [en]

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. 565-574 p.
National Category
Algebra and Logic
Research subject
Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-140143DOI: 10.1145/2933575.2934545ISI: 000387609200057ISBN: 978-1-4503-4391-6 (print)OAI: oai:DiVA.org:su-140143DiVA: diva2:1077736
Conference
Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), New York City, USA, July 5-8, 2016
Available from: 2017-02-28 Created: 2017-02-28 Last updated: 2017-03-31Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textarXiv:1605.03227

Search in DiVA

By author/editor
Hou, Kuen-Bang (Favonia)Lumsdaine, Peter LeFanu
By organisation
Department of Mathematics
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 4 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf