Construction of the circle in UniMath

Bezem, Marc; Buchholtz, Ulrik; Grayson, Daniel R.; Shulman, Michael

Abstract

We show that the type TZ of Z-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence Axiom and propositional truncation, yielding a stand-alone construction of the circle not using higher inductive types.

Citation

Bezem, M., Buchholtz, U., Grayson, D. R., & Shulman, M. (2021). Construction of the circle in UniMath. Journal of Pure and Applied Algebra, 225(10), Article 106687. https://doi.org/10.1016/j.jpaa.2021.106687

• Journal Article Type: Article
• Acceptance Date: Nov 18, 2020
• Online Publication Date: Jan 11, 2021
• Publication Date: 2021-10
• Deposit Date: Oct 11, 2024
• Publicly Available Date: Oct 16, 2024
• Journal: Journal of Pure and Applied Algebra
• Print ISSN: 0022-4049
• Electronic ISSN: 1873-1376
• Publisher: Elsevier
• Peer Reviewed: Peer Reviewed
• Volume: 225
• Issue: 10
• Article Number: 106687
• DOI: https://doi.org/10.1016/j.jpaa.2021.106687
• Public URL: https://nottingham-repository.worktribe.com/output/39730591
• Publisher URL: https://www.sciencedirect.com/science/article/pii/S0022404921000232?via%3Dihub