Covering spaces in homotopy type theory

Kuen Bang Hou Favonia, Robert Harper

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publication22nd International Conference on Types for Proofs and Programs, TYPES 2016
EditorsHerman Geuvers, Jelena Ivetic, Silvia Ghilezan
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770651
DOIs
StatePublished - Oct 1 2018
Event22nd International Conference on Types for Proofs and Programs, TYPES 2016 - Novi Sad, Serbia
Duration: May 23 2016May 26 2016

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume97
ISSN (Print)1868-8969

Conference

Conference22nd International Conference on Types for Proofs and Programs, TYPES 2016
CountrySerbia
CityNovi Sad
Period5/23/165/26/16

Keywords

  • Covering space
  • Fundamental group
  • Homotopy type theory
  • Mechanized reasoning

Fingerprint Dive into the research topics of 'Covering spaces in homotopy type theory'. Together they form a unique fingerprint.

  • Cite this

    Favonia, K. B. H., & Harper, R. (2018). Covering spaces in homotopy type theory. In H. Geuvers, J. Ivetic, & S. Ghilezan (Eds.), 22nd International Conference on Types for Proofs and Programs, TYPES 2016 [11] (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 97). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.TYPES.2016.11