# Homotopy Type Theory circle (changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

## Idea

The circle is one of the simplest higher inductive types it consists of a single point and a single non-trivial path between.

## Definition

The circle denoted $S^1$ is defined as the higher inductive type generated by:

• A point $base : S^1$
• A path $loop : base = base$

Alternative definitions include the suspension of $\mathbf{2}$ and as a coequalizer?.

## Properties

Its induction principle? says that for any $P:S^1\to Type$ equipped with a point $base' : P(base)$ and a dependent path? $loop':base'= 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 f(loop)=l ap_f(loop)=l

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

There are several proofs in the 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.)

Two of them were blogged about:

### Alternative definition 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.

## References

HoTT book

category: homotopy theory

Last revised on January 19, 2019 at 15:35:09. See the history of this page for a list of all contributions to it.