Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2016.22
URN: urn:nbn:de:0030-drops-65626
URL: https://drops.dagstuhl.de/opus/volltexte/2016/6562/
Hou (Favonia), Kuen-Bang ; Shulman, Michael
The Seifert-van Kampen Theorem in Homotopy Type Theory
| pdf-format: |
|
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.
BibTeX - Entry
@InProceedings{houfavonia_et_al:LIPIcs:2016:6562,
author = {Kuen-Bang {Hou (Favonia)} and Michael Shulman},
title = {{The Seifert-van Kampen Theorem in Homotopy Type Theory}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {22:1--22:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Jean-Marc Talbot and Laurent Regnier},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6562},
URN = {urn:nbn:de:0030-drops-65626},
doi = {10.4230/LIPIcs.CSL.2016.22},
annote = {Keywords: homotopy type theory, fundamental group, homotopy pushout, mechanized reasoning}
}
| Keywords: | homotopy type theory, fundamental group, homotopy pushout, mechanized reasoning | |
| Seminar: | 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) | |
| Issue date: | 2016 | |
| Date of publication: | 29.08.2016 |
