Construction of the circle in UniMath
Journal article, Peer reviewed
Published version
Åpne
Permanent lenke
https://hdl.handle.net/11250/2984689Utgivelsesdato
2021Metadata
Vis full innførselSamlinger
- Department of Informatics [917]
- Registrations from Cristin [9489]
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.