2026-07-22T16:58:31Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6562 2024-03-06T10:38:43Z ddc:004 open_access

The Seifert-van Kampen Theorem in Homotopy Type Theory Hou (Favonia), Kuen-Bang Shulman, Michael homotopy type theory fundamental group homotopy pushout mechanized reasoning 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kuen-Bang Hou (Favonia) and Michael Shulman 2016 Is Part Of LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2016.22 urn:nbn:de:0030-drops-65626 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.22 eng https://creativecommons.org/licenses/by/3.0/legalcode