Construction of the circle in UniMath
Journal article, Peer reviewed
Published version
View/
Date
2021Metadata
Show full item recordCollections
- Department of Informatics [1010]
- Registrations from Cristin [11722]
Original version
Journal of Pure and Applied Algebra. 2021, 225 (10), 106687. 10.1016/j.jpaa.2021.106687Abstract
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.
Publisher
ElsevierJournal
Journal of Pure and Applied AlgebraCopyright
Copyright 2021 The Author(s)
Except where otherwise noted, this item's license is described as Navngivelse 4.0 Internasjonal