Document Open Access Logo

Covering Spaces in Homotopy Type Theory

Authors Kuen-Bang Hou (Favonia), Robert Harper

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2016.11.pdf
  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Author Details

Kuen-Bang Hou (Favonia)
Robert Harper

Cite As Get BibTex

Kuen-Bang Hou (Favonia) and Robert Harper. Covering Spaces in Homotopy Type Theory. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.TYPES.2016.11

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.

Subject Classification

Keywords
  • homotopy type theory
  • covering space
  • fundamental group
  • mechanized reasoning

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. The Coq proof assistant. URL: https://coq.inria.fr/.
  2. Mathieu Anel, Georg Biedermann, Eric Finster, and André Joyal. A generalized Blakers-Massey theorem. arXiv, 2017. URL: http://arxiv.org/abs/1703.09050v2.
  3. Steve Awodey and Michael A. Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1):45-55, 1 2009. URL: http://dx.doi.org/10.1017/S0305004108001783.
  4. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Bas Spitters, et al. The HoTT library. URL: https://github.com/HoTT/HoTT.
  5. Guillaume Brunerie. On the homotopy groups of spheres in homotopy type theory. PhD thesis, Université Nice Sophia Antipolis, 2016. URL: http://arxiv.org/abs/1606.05916v1.
  6. Guillaume Brunerie, Kuen-Bang Hou (Favonia), Evan Cavallo, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et al. Homotopy type theory in Agda. URL: https://github.com/HoTT/HoTT-Agda.
  7. Guillaume Brunerie, Kuen-Bang Hou (Favonia), Evan Cavallo, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et al. Homotopy type theory in Agda. URL: http://dx.doi.org/10.6084/m9.figshare.5161546.
  8. Ulrik Buchholtz and Egbert Rijke. The Cayley-Dickson construction in homotopy type theory. URL: http://arxiv.org/abs/1610.01134v1.
  9. Ulrik Buchholtz, Floris van Doorn, and Jakob von Raumer. Homotopy type theory in Lean. To appear in the Proceedings of the 8th International Conference on Interactive Theorem Proving. URL: http://arxiv.org/abs/1704.06781v1.
  10. Evan Cavallo. Synthetic cohomology in homotopy type theory. Master’s thesis, Carnegie Mellon University, 2015. URL: http://www.cs.cmu.edu/~ecavallo/works/thesis.pdf.
  11. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Automated Deduction - CADE-25, volume 9195 of Lecture Notes in Computer Science, pages 378-388, Switzerland, 2015. Springer International Publishing. URL: http://dx.doi.org/10.1007/978-3-319-21401-6_26.
  12. Nicola Gambino and Richard Garner. The identity type weak factorisation system. Theoretical Computer Science, 409(1):94-109, 2008. URL: http://dx.doi.org/10.1016/j.tcs.2008.08.030.
  13. Jean-Yves Girard. Interprétation Fonctionnelle et élimination des Coupures de l'Arithmétique d'Ordre Supérieur. PhD thesis, Université Paris 7, 1972. Google Scholar
  14. Allen Hatcher. Algebraic Topology. Cambridge University Press, Cambridge, UK, 2002. URL: http://www.math.cornell.edu/~hatcher/AT/ATpage.html.
  15. Kuen-Bang Hou (Favonia). Covering spaces in homotopy type theory. In Maria del Mar González, Paul C. Yang, Nicola Gambino, and Joachim Kock, editors, Extended Abstracts Fall 2013: Geometrical Analysis; Type Theory, Homotopy Theory and Univalent Foundations, pages 77-82, Cham, 2015. Birkhäuser. URL: http://dx.doi.org/10.1007/978-3-319-21284-5_15.
  16. Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine. A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 565-574, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2933575.2934545.
  17. Kuen-Bang Hou (Favonia) and Michael Shulman. The Seifert-van Kampen theorem in homotopy type theory. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:16, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2016.22.
  18. Antonius J. C. Hurkens. A simplification of Girard’s paradox. In Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 266-278. Springer, Berlin, Heidelberg, 1995. URL: http://dx.doi.org/10.1007/BFb0014058.
  19. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky), 2012. URL: http://arxiv.org/abs/1211.2851v4.
  20. Nicolai Kraus. The general universal property of the propositional truncation. URL: http://arxiv.org/abs/1411.2682v3.
  21. Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, and Thorsten Altenkirch. Notions of anonymous existence in Martin-Löf type theory. URL: http://arxiv.org/abs/1610.03346v1.
  22. Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, and Thorsten Altenkirch. Generalizations of Hedberg’s theorem. In Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings, pages 173-188, 2013. URL: http://dx.doi.org/10.1007/978-3-642-38946-7_14.
  23. Daniel R. Licata and Guillaume Brunerie. π_n(sⁿ) in homotopy type theory. In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs: Third International Conference, CPP 2013, pages 1-16, Cham, 2013. Springer International Publishing. URL: http://dx.doi.org/10.1007/978-3-319-03545-1_1.
  24. Daniel R. Licata and Guillaume Brunerie. A cubical approach to synthetic homotopy theory. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), LICS '15, pages 92-103, Washington, DC, USA, 2015. IEEE Computer Society. URL: http://dx.doi.org/10.1109/LICS.2015.19.
  25. Daniel R. Licata and Eric Finster. Eilenberg-MacLane spaces in homotopy type theory. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 66:1-66:9, New York, NY, USA, 2014. ACM. URL: http://dx.doi.org/10.1145/2603088.2603153.
  26. Daniel R. Licata and Michael Shulman. Calculating the fundamental group of the circle in homotopy type theory. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '13, pages 223-232, Washington, DC, USA, 2013. IEEE Computer Society. URL: http://dx.doi.org/10.1109/LICS.2013.28.
  27. Peter LeFanu Lumsdaine. Higher inductive types: a tour of the menagerie. URL: https://homotopytypetheory.org/2011/04/24/higher-inductive-types-a-tour-of-the-menagerie/.
  28. Peter LeFanu Lumsdaine. Weak ω-categories from intensional type theory. In Typed Lambda Calculi and Applications, volume 5608 of Lecture Notes in Computer Science, pages 172-187. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02273-9_14.
  29. Per Martin-Löf. An intuitionistic theory of types: Predicative part. In Logic Colloquium '73, Proceedings of the Logic Colloquium, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. Elsevier, 1975. URL: http://dx.doi.org/10.1016/S0049-237X(08)71945-1.
  30. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007. URL: http://www.cse.chalmers.se/~ulfn/papers/thesis.html.
  31. Charles Rezk. Proof of the Blakers-Massey theorem. Prepublished, 2015. URL: http://www.math.uiuc.edu/~rezk/freudenthal-and-blakers-massey.pdf.
  32. Egbert Rijke. Homotopy type theory. Master’s thesis, Utrecht University, 2012. URL: http://hottheory.files.wordpress.com/2012/08/hott2.pdf.
  33. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, git commit hash g662cdd8 edition, 2013.
  34. Benno van den Berg and Richard Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370-394, 2011. URL: http://dx.doi.org/10.1112/plms/pdq026.
  35. Benno van den Berg and Richard Garner. Topological and simplicial models of identity types. ACM Transactions on Computational Logic, 13(1):3:1-3:44, 2012. URL: http://dx.doi.org/10.1145/2071368.2071371.
  36. Vladimir Voevodsky. A very short note on homotopy λ-calculus, 09 2006. URL: http://www.math.ias.edu/vladimir/files/2006_09_Hlambda.pdf.
  37. Jakob von Raumer. Formalization of non-abelian topology for homotopy type theory. Master’s thesis, Karlsruhe Institute of Technology, 2015. URL: http://von-raumer.de/msc-thesis.pdf.
  38. Michael A. Warren. Homotopy theoretic aspects of constructive type theory. PhD thesis, Carnegie Mellon University, 2008. URL: http://mawarren.net/papers/phd.pdf.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact