TY - GEN

T1 - The Seifert-van Kampen theorem in homotopy type theory

AU - Favonia, F.

AU - Shulman, Michael

PY - 2016/8/1

Y1 - 2016/8/1

N2 - 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.

AB - 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.

KW - Fundamental group

KW - Homotopy pushout

KW - Homotopy type theory

KW - Mechanized reasoning

UR - http://www.scopus.com/inward/record.url?scp=85012905251&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85012905251&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CSL.2016.22

DO - 10.4230/LIPIcs.CSL.2016.22

M3 - Conference contribution

AN - SCOPUS:85012905251

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - Computer Science Logic 2016, CSL 2016

A2 - Talbot, Jean-Marc

A2 - Regnier, Laurent

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic

Y2 - 29 August 2016 through 1 September 2016

ER -