Homotopy Type Theory A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory < , LICS 2016 A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type TheoryKuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine

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.

See also

  • Blakers-Massey Theorem?
  • connectivity?

category: reference

Revision on June 9, 2022 at 18:05:29 by Anonymous?. See the history of this page for a list of all contributions to it.