Tom de Jong, 2 April 2021

The following modules construct the circle 𝕊¹ as the type of ℤ-torsors,
following "Construction of the circle in UniMath" by Bezem, Buchholtz, Grayson
and Shulman (doi:10.1016/j.jpaa.2021.106687).

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Circle.index where

import Circle.Integers
import Circle.Integers-Properties
import Circle.Integers-SymmetricInduction

import Circle.Construction
import Circle.Induction

\end{code}