Construction of the circle in UniMath
(2021)
Journal Article
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
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-al... Read More about Construction of the circle in UniMath.