Covering Spaces in Homotopy Type Theory

Research output: Contribution to journalArticle

1 Scopus citations


Covering spaces play an important role in classical homotopy theory, whose algebraic characteristics have deep connections with fundamental groups of underlying spaces. It is natural to ask whether these connections can be stated in homotopy type theory (HoTT), an exciting new framework coming with an interpretation in homotopy theory. This note summarizes the author's attempt to recover the classical results (e.g., the classification theorem) so as to explore the expressiveness of the new foundation. Some interesting techniques employed in the current proofs seem applicable to other constructions as well.

Original languageEnglish (US)
Pages (from-to)77-82
Number of pages6
JournalTrends in Mathematics
StatePublished - Jan 1 2015
Externally publishedYes

Fingerprint Dive into the research topics of 'Covering Spaces in Homotopy Type Theory'. Together they form a unique fingerprint.

  • Cite this