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 language||English (US)|
|Title of host publication||Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016|
|Publisher||Institute of Electrical and Electronics Engineers Inc.|
|Number of pages||10|
|State||Published - Jul 5 2016|
|Event||31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 - New York, United States|
Duration: Jul 5 2016 → Jul 8 2016
|Name||Proceedings - Symposium on Logic in Computer Science|
|Conference||31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016|
|Period||7/5/16 → 7/8/16|
Bibliographical notePublisher Copyright:
© 2016 ACM.