文章基本信息

标题：The Seifert-van Kampen Theorem in Homotopy Type Theory
本地全文：下载
作者：Kuen-Bang {Hou ; Michael Shulman
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2016
卷号：62
页码：22:1-22:16
DOI：10.4230/LIPIcs.CSL.2016.22
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：homotopy type theory; fundamental group; homotopy pushout; mechanized reasoning