Covering spaces in homotopy type theory

Kuen Bang Hou Favonia; Robert Harper

doi:10.4230/LIPIcs.TYPES.2016.11

Covering spaces in homotopy type theory

Kuen Bang Hou Favonia, Robert Harper

Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Scopus citations

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 language	English (US)
Title of host publication	22nd International Conference on Types for Proofs and Programs, TYPES 2016
Editors	Herman Geuvers, Jelena Ivetic, Silvia Ghilezan
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)	9783959770651
DOIs	https://doi.org/10.4230/LIPIcs.TYPES.2016.11
State	Published - Oct 1 2018
Event	22nd International Conference on Types for Proofs and Programs, TYPES 2016 - Novi Sad, Serbia Duration: May 23 2016 → May 26 2016

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	97
ISSN (Print)	1868-8969

Conference

Conference	22nd International Conference on Types for Proofs and Programs, TYPES 2016
Country/Territory	Serbia
City	Novi Sad
Period	5/23/16 → 5/26/16

Bibliographical note

Publisher Copyright:
© Kuen-Bang Hou (Favonia) and Robert Harper; licensed under Creative Commons License CC-BY 22nd International Conference on Types for Proofs and Programs (TYPES 2016).

Keywords

Covering space
Fundamental group
Homotopy type theory
Mechanized reasoning

Publisher link

10.4230/LIPIcs.TYPES.2016.11

Find It

Find It at U of M Libraries

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 Article 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

Covering spaces in homotopy type theory. / Favonia, Kuen Bang Hou; Harper, Robert.
22nd International Conference on Types for Proofs and Programs, TYPES 2016. ed. / Herman Geuvers; Jelena Ivetic; Silvia Ghilezan. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2018. 11 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 97).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Favonia, KBH & 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, 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, 5/23/16. https://doi.org/10.4230/LIPIcs.TYPES.2016.11

@inproceedings{6218ef44fa81415b86cb5211a9d68444,

title = "Covering spaces in homotopy type theory",

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.",

keywords = "Covering space, Fundamental group, Homotopy type theory, Mechanized reasoning",

author = "Favonia, {Kuen Bang Hou} and Robert Harper",

note = "Publisher Copyright: {\textcopyright} Kuen-Bang Hou (Favonia) and Robert Harper; licensed under Creative Commons License CC-BY 22nd International Conference on Types for Proofs and Programs (TYPES 2016).; 22nd International Conference on Types for Proofs and Programs, TYPES 2016 ; Conference date: 23-05-2016 Through 26-05-2016",

year = "2018",

month = oct,

day = "1",

doi = "10.4230/LIPIcs.TYPES.2016.11",

language = "English (US)",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

editor = "Herman Geuvers and Jelena Ivetic and Silvia Ghilezan",

booktitle = "22nd International Conference on Types for Proofs and Programs, TYPES 2016",

}

TY - GEN

T1 - Covering spaces in homotopy type theory

AU - Favonia, Kuen Bang Hou

AU - Harper, Robert

N1 - Publisher Copyright: © Kuen-Bang Hou (Favonia) and Robert Harper; licensed under Creative Commons License CC-BY 22nd International Conference on Types for Proofs and Programs (TYPES 2016).

PY - 2018/10/1

Y1 - 2018/10/1

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

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

KW - Covering space

KW - Fundamental group

KW - Homotopy type theory

KW - Mechanized reasoning

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

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

U2 - 10.4230/LIPIcs.TYPES.2016.11

DO - 10.4230/LIPIcs.TYPES.2016.11

M3 - Conference contribution

AN - SCOPUS:85057015175

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 22nd International Conference on Types for Proofs and Programs, TYPES 2016

A2 - Geuvers, Herman

A2 - Ivetic, Jelena

A2 - Ghilezan, Silvia

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

T2 - 22nd International Conference on Types for Proofs and Programs, TYPES 2016

Y2 - 23 May 2016 through 26 May 2016

ER -

Covering spaces in homotopy type theory

Abstract

Publication series

Conference

Bibliographical note

Keywords

Publisher link

Find It

Other files and links

Fingerprint

Cite this