文章基本信息

标题：Covering Spaces in Homotopy Type Theory
本地全文：下载
作者：Kuen-Bang {Hou ; Robert Harper
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：97
页码：1-16
DOI：10.4230/LIPIcs.TYPES.2016.11
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Broadly speaking, algebraic topology consists of associating algebraic structures to topological spaces that give information about their structure. An elementary, but fundamental, example is provided by the theory of covering spaces, which associate groups to covering spaces in such a way that the universal cover corresponds to the fundamental group of the space. One natural question to ask is whether these connections can be stated in homotopy type theory, a new area linking type theory to homotopy theory. In this paper, we give an affirmative answer with a surprisingly concise definition of covering spaces in type theory; we are able to prove various expected properties about the newly defined covering spaces, including the connections with fundamental groups. An additional merit is that our work has been fully mechanized in the proof assistant Agda.
关键词：homotopy type theory; covering space; fundamental group; mechanized reasoning