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}$.

### 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 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 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.)

A 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}$):