  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.
