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 inductive constructed from a terms in the circle, whose interpretation is as the base point of the circle, together with a term in the identity type of paths between these two terms, which interprets as the 1-cell of the circle

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

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

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