Construction of the Circle in UniMath

TL;DR

This paper constructs the circle as a type of Z-torsors in UniMath using Voevodsky's Univalence Axiom and propositional truncation, providing a stand-alone, higher inductive type-free approach.

Contribution

It introduces a novel construction of the circle in UniMath based on Z-torsors and homotopy-theoretic principles, avoiding higher inductive types.

Findings

The type of Z-torsors has the universal property of the circle.

The construction is independent of higher inductive types.

It leverages the Univalence Axiom and propositional truncation.

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.