nLab circle type

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

See also

• circle, unit circle, circle group, circle object

• interval type

• minimal simplicial circle

• suspension type

• sphere type

• homotopy groups of spheres

• Jordan curve

• lemniscate type?

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

• Dan Licata, Mike Shulman, Calculating the Fundamental Group of the Circle in Homotopy Type Theory, LICS ‘13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science June 2013 (arXiv:1301.3443, doi:10.1109/LICS.2013.28)

  blog announcements:

  A formal proof that $\pi_1(S^1) = \mathbb{Z}$

  A simpler proof that $\pi_1(S^1) = \mathbb{Z}$

Formalization in proof assistants:

in Coq:

• The HoTT Coq library: theories/hit/Circle.v

in Agda:

• The HoTT Agda library: homotopy/LoopSpaceCircle.agda

Exposition and review:

• Univalent Foundations Project, §8.1 Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]

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

• Marc Bezem, Ulrik Buchholtz, Daniel Grayson, Michael Shulman, Construction of the Circle in UniMath, Journal of Pure and Applied Algebra Volume 225, Issue 10, October 2021, 106687 (arXiv:1910.01856)

Alternative construction of the circle type as a coequalizer:

• Mike Shulman, Section 9 of Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)