LIPIcs.CSL.2016.22.pdf
- Filesize: 0.67 MB
- 16 pages
Document
The Seifert-van Kampen Theorem in Homotopy Type Theory
Authors
-
Part of:
Volume:
25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2016-08-29
Cite AsGet BibTex
Kuen-Bang Hou (Favonia) and Michael Shulman. The Seifert-van Kampen Theorem in Homotopy Type Theory. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 22:1-22:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CSL.2016.22
https://doi.org/10.4230/LIPIcs.CSL.2016.22
Abstract
Homotopy type theory is a recent research area connecting type theory with homotopy theory by interpreting types as spaces. In particular, one can prove and mechanize type-theoretic analogues of homotopy-theoretic theorems, yielding "synthetic homotopy theory". Here we consider the Seifert-van Kampen theorem, which characterizes the loop structure of spaces obtained by gluing. This is useful in homotopy theory because many spaces are constructed by gluing, and the loop structure helps distinguish distinct spaces. The synthetic proof showcases many new characteristics of synthetic homotopy theory, such as the "encode-decode" method, enforced homotopy-invariance, and lack of underlying sets.
Keywords
- homotopy type theory
- fundamental group
- homotopy pushout
- mechanized reasoning
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25:1010-1039, 6 2015. URL: http://dx.doi.org/10.1017/S0960129514000486.
- Steve Awodey and Michael A. Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1):45-55, jan 2009. URL: http://dx.doi.org/10.1017/S0305004108001783.
- Marc Bezem, Thierry Coquand, and Simon Huber. A model of type theory in cubical sets. In 19th International Conference on Types for Proofs and Programs, volume 26 of Leibniz International Proceedings in Informatics, pages 107-128. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. URL: http://dx.doi.org/10.4230/LIPIcs.TYPES.2013.107.
- Evan Cavallo. The Mayer-Vietoris sequence in HoTT. In Oxford Quantum Video. The QMAC and Clay Mathematics Institute and The EPSRC, 2014. URL: https://youtu.be/6QCFV4op1Uo.
- The Coq proof assistant. URL: https://coq.inria.fr/.
- 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. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21401-6_26.
- 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.
- Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory, volume 36 of Oxford Logic Guides, pages 83-111. Oxford University Press, 1998. URL: http://arxiv.org/abs/pLnKggT_In4C.
- 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, May 2016. URL: http://arxiv.org/abs/1605.03227.
- Chris Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky), 2012. URL: http://arxiv.org/abs/1211.2851.
- Daniel R. Licata. Running circles around (in) your proof assistant; or, quotients that compute, 2011. URL: http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/.
- Daniel R. Licata and Guillaume Brunerie. π_n(Sⁿ) in homotopy type theory. CPP, 2013. URL: http://dlicata.web.wesleyan.edu/pubs/lb13cpp/lb13cpp.pdf.
- Daniel R. Licata and Guillaume Brunerie. A cubical approach to synthetic homotopy theory. LICS, 2015. URL: http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf.
- Daniel R. Licata and Eric Finster. Eilenberg-MacLane spaces in homotopy type theory. LICS, 2014. URL: http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf.
- Daniel R. Licata and Michael Shulman. Calculating the fundamental group of the circle in homotopy type theory. In LICS'13, 2013. URL: http://arxiv.org/abs/1301.3443.
- 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.
- Charles Rezk. Proof of the Blakers-Massey theorem, 2014. URL: http://www.math.uiuc.edu/~rezk/freudenthal-and-blakers-massey.pdf.
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for Mathematics. Institute for Advanced Study, git commit hash g662cdd8 edition, 2013. URL: http://homotopytypetheory.org/book.
- 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.
- Michael A. Warren. Homotopy theoretic aspects of constructive type theory. PhD thesis, Carnegie Mellon University, 2008. URL: http://mawarren.net/papers/phd.pdf.