The Seifert-van Kampen theorem in homotopy type theory

F. Favonia, Michael Shulman

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Scopus citations

Abstract

Homotopy type theory is a recent research area connecting type theory with homotopy theory by interpreting types as spaces. In particular, one can prove and mechanize type-theoretic analogues of homotopy-theoretic theorems, yielding "synthetic homotopy theory". Here we consider the Seifert-van Kampen theorem, which characterizes the loop structure of spaces obtained by gluing. This is useful in homotopy theory because many spaces are constructed by gluing, and the loop structure helps distinguish distinct spaces. The synthetic proof showcases many new characteristics of synthetic homotopy theory, such as the "encode-decode" method, enforced homotopy-invariance, and lack of underlying sets.

Original languageEnglish (US)
Title of host publicationComputer Science Logic 2016, CSL 2016
EditorsJean-Marc Talbot, Laurent Regnier
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770224
DOIs
StatePublished - Aug 1 2016
Externally publishedYes
Event25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic - Marseille, France
Duration: Aug 29 2016Sep 1 2016

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume62
ISSN (Print)1868-8969

Conference

Conference25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic
Country/TerritoryFrance
CityMarseille
Period8/29/169/1/16

Keywords

  • Fundamental group
  • Homotopy pushout
  • Homotopy type theory
  • Mechanized reasoning

Fingerprint

Dive into the research topics of 'The Seifert-van Kampen theorem in homotopy type theory'. Together they form a unique fingerprint.

Cite this