TY - GEN

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

AU - Favonia, Kuen Bang Hou

AU - Finster, Eric

AU - Licata, Daniel R.

AU - Lumsdaine, Peter Lefanu

N1 - Publisher Copyright:
© 2016 ACM.
Copyright:
Copyright 2017 Elsevier B.V., All rights reserved.

PY - 2016/7/5

Y1 - 2016/7/5

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84994571417&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84994571417&partnerID=8YFLogxK

U2 - 10.1145/2933575.2934545

DO - 10.1145/2933575.2934545

M3 - Conference contribution

AN - SCOPUS:84994571417

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 565

EP - 574

BT - Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016

Y2 - 5 July 2016 through 8 July 2016

ER -