A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
| Autor: | Peter LeFanu Lumsdaine, Eric Finster, Daniel R. Licata, Kuen-Bang Hou Favonia |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
FOS: Computer and information sciences
Mathematical logic Computer Science - Logic in Computer Science Pure mathematics Homotopy 010102 general mathematics Pushout 0102 computer and information sciences Type (model theory) Mathematical proof Mathematics::Algebraic Topology 01 natural sciences Logic in Computer Science (cs.LO) Type theory 010201 computation theory & mathematics Mathematics::Category Theory FOS: Mathematics Homotopy type theory Algebraic Topology (math.AT) F.4.1 Mathematics - Algebraic Topology 55U35 (Abstract and axiomatic homotopy theory) 03B15 (Higher-order logic and type theory) 03B70 (Logic in computer science) 0101 mathematics Freudenthal suspension theorem Mathematics |
| Zdroj: | LICS |
| DOI: | 10.1145/2933575.2934545 |
| Popis: | 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. To appear in LICS 2016 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|