Marc Bezem
Construction of the circle in UniMath
Bezem, Marc; Buchholtz, Ulrik; Grayson, Daniel R.; Shulman, Michael
Authors
Dr ULRIK TORBEN BUCHHOLTZ ULRIK.BUCHHOLTZ@NOTTINGHAM.AC.UK
Assistant Professor
Daniel R. Grayson
Michael Shulman
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 |
Files
Construction of the circle in UniMath
(518 Kb)
PDF
Publisher Licence URL
https://creativecommons.org/licenses/by/4.0/
You might also like
Synthetic fibered (∞,1)-category theory
(2023)
Journal Article
On symmetries of spheres in univalent foundations
(-0001)
Presentation / Conference Contribution
The long exact sequence of homotopy n-groups
(2023)
Journal Article
Epimorphisms and acyclic types in univalent foundations
(2024)
Journal Article
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: discovery-access-systems@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search