Contents

# Contents

## Idea

The circle type is an axiomatization of the homotopy type of the (shape of) the circle in the context of homotopy type theory.

## Definition

As a higher inductive type, the circle is given by

Inductive Circle : Type
| base : Circle
| loop : Id Circle base base

This says that the type is inductively constructed from

1. a term of circle type whose interpretation is as the base point of the circle,

2. a term of the identity type of paths between these two terms, which interprets as the 1-cell of the circle

$base \stackrel{loop}{\to} base \,$

Hence a non-constant path from the base point to itself.

### As a suspension

The circle type could also be defined as the suspension type $\Sigma \mathbf{2}$ of the type of booleans $\mathbf{2}$.

### As a coequalizer

The circle type could also be defined as the coequalizer type of any two endofunctions on the unit type

$\mathbf{1} \rightrightarrows \mathbf{1} \to S^1$

### Using torsors

The circle can also be defined without HITs using only univalence, as the type of $\mathbb{Z}$-torsors. One can then prove that this type satisfies the same induction principle (propositionally). This is due to Dan Grayson.

## Properties

Its induction principle says (e.g. UFP13, p. 177) that for

• any $P \colon S^1 \to Type$

• equipped with a point $base' \colon P(base)$

• and a dependent path $loop' \,\colon\, base' =_{loop} base'$,

there is $f:\prod_{(x:S^1)} P(x)$ such that:

$f(base)=base'\qquad apd_f(loop) = loop'$

As a special case, its recursion principle says that given any type $X$ with a point $x:X$ and a loop $l:x=x$, there is $f:S^1 \to X$ with

$f(base)=x\qquad ap_f(loop)=l$

### $\Omega(S^1)=\mathbb{Z}$

There are several proofs in the HoTT book that the loop space $\Omega(S^1)$ of the circle is the integers $\mathbb{Z}$. (Any such proof requires the univalence axiom, since without that it is consistent that $S^1$ is contractible. Indeed, $S^1$ is contractible if and only if UIP holds.)

## References

The formalization of the shape homotopy type $ʃ S^1 \simeq \mathbf{B}\mathbb{Z}$ of the circle as a higher inductive type in homotopy type theory, along with a proof that $\Omega ʃS^1\simeq {\mathbb{Z}}$ (and hence $\pi_1(ʃS^1) \simeq \mathbb{Z}$):

Formalization in proof assistants:

in Coq:

in Agda:

Exposition and review:

Alternative construction of the circle type as the type of $\mathbb{Z}$-torsors:

Alternative construction of the circle type as a coequalizer:

Last revised on March 2, 2023 at 05:25:52. See the history of this page for a list of all contributions to it.