Current browse context:
cs.LO
Change to browse by:
References & Citations
Computer Science > Logic in Computer Science
Title: A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
(Submitted on 10 May 2016)
Abstract: 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.
Submission history
From: Peter LeFanu Lumsdaine [view email][v1] Tue, 10 May 2016 22:13:17 GMT (177kb,D)
Link back to: arXiv, form interface, contact.