Construction of the Circle in UniMath

Marc Bezem, Ulrik Buchholtz, Daniel R. Grayson +1

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.…