Construction of the Circle in UniMath
classification
🧮 math.LO
cs.LOmath.AT
keywords
circleconstructionmathbbaxiomcharacterizesdependentequivalencehigher
read the original abstract
We show that the type $\mathrm{T}\mathbb{Z}$ of $\mathbb{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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.