A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

Kuen Bang Hou Favonia, Eric Finster, Daniel R. Licata, Peter Lefanu Lumsdaine

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Scopus citations

Abstract

This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces sharing a common part (represented by a pushout type, which is a generalization of a disjoint sum type) to those of the common part itself. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which was used in previous formalizations. The proof is more direct than existing ones that apply in general category-theoretic settings for homotopy theory, and its mechanization is concise and high-level, due to novel combinations of ideas from homotopy theory and from type theory.

Original languageEnglish (US)
Title of host publicationProceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages565-574
Number of pages10
ISBN (Electronic)9781450343916
DOIs
StatePublished - Jul 5 2016
Externally publishedYes
Event31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 - New York, United States
Duration: Jul 5 2016Jul 8 2016

Publication series

NameProceedings - Symposium on Logic in Computer Science
Volume05-08-July-2016
ISSN (Print)1043-6871

Conference

Conference31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
CountryUnited States
CityNew York
Period7/5/167/8/16

Fingerprint Dive into the research topics of 'A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory'. Together they form a unique fingerprint.

Cite this