Document Open Access Logo

Formalizing Equivalences Without Tears

Author Tom de Jong

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.TYPES.2024.1.pdf
  • Filesize: 0.79 MB
  • 6 pages
HTML5 Logo HTML (experimental)
LIPIcs.TYPES.2024.1.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • 3-for-2 property
  • 2-out-of-3 property
  • definitional equality
  • equivalence
  • formalization of mathematics
  • synthetic homotopy theory
  • type theory

Metrics

Abstract

This expository note describes two convenient techniques in the context of homotopy type theory for proving - and formalizing - that a given map is an equivalence. The first technique decomposes the map as a series of basic equivalences, while the second refines this approach using the 3-for-2 property of equivalences. The techniques are illustrated by proving a basic result in synthetic homotopy theory.

Cite As Get BibTex

Tom de Jong. Formalizing Equivalences Without Tears. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 1:1-1:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TYPES.2024.1

Author Details

Tom de Jong
  • School of Computer Science, University of Nottingham, UK

Funding

This work was supported by The Royal Society (grant reference URF\R1\191055). The HIM programme was funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) under Germany’s Excellence Strategy - EXC-2047/1 - 390685813.

Acknowledgements

I am grateful to Josh Chen, Stefania Damato, Martín Escardó, Nicolai Kraus, Fredrik Nordvall Forsberg, Stiéphen Pradal and Jon Sterling for comments on this note. I also thank the participants, organizers and support staff of the HIM trimester programme Prospects of Formal Mathematics for the opportunity to present the ideas in this note. Finally, I thank the anonymous reviewers for their helpful suggestions.

References

  1. Martín H. Escardó and contributors. TypeTopology. http://www.cs.bham.ac.uk/~mhe/TypeTopology/index.html. Agda development. URL: https://github.com/martinescardo/TypeTopology.
  2. Martín Hötzel Escardó. Introduction to univalent foundations of mathematics with Agda, 2019. URL: https://arxiv.org/abs/1911.00580.
  3. Martin Hofmann. Extensional concepts in intensional type theory. PhD thesis, University of Edinburgh, 1995. Published in Springer’s Distinguished Dissertations series in 1997. URL: https://doi.org/10.1007/978-1-4471-0963-1.
  4. André Joyal. Categorical aspects of type theory, 2013. Talk in the Progress in Higher Categories session at the Canadian Mathematical Society (CMS) Summer Meeting in Halifax. URL: https://home.sandiego.edu/~shulman/cmshighercategories2013/Joyal.pdf.
  5. Egbert Rijke, Elisabeth Bonnevier, Jonathan Prieto-Cubides, Fredrik Bakke, and others. The agda-unimath library. URL: https://unimath.github.io/agda-unimath/.
  6. Egbert Rijke, J. Daniel Christensen, Luis Scoccola, and Morgan Opie. Localization in homotopy type theory. Higher Structures, 4(1):1-32, 2020. URL: https://doi.org/10.21136/hs.2020.01.
  7. Michael Shulman. Homotopy type theory: The logic of space. In Mathieu Anel and Gabriel Catren, editors, New Spaces in Mathematics, pages 322-404. Cambridge University Press, 2021. URL: https://doi.org/10.1017/9781108854429.009.
  8. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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