Construction of the circle in UniMath
Journal article, Peer reviewed
Published version
![Thumbnail](/bora-xmlui/bitstream/handle/11250/2984689/1-s2.0-S0022404921000232-main.pdf.jpg?sequence=6&isAllowed=y)
Åpne
Permanent lenke
https://hdl.handle.net/11250/2984689Utgivelsesdato
2021Metadata
Vis full innførselSamlinger
- Department of Informatics [928]
- Registrations from Cristin [9791]
Originalversjon
Journal of Pure and Applied Algebra. 2021, 225 (10), 106687. 10.1016/j.jpaa.2021.106687Sammendrag
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 standalone construction of the circle not using higher inductive types.