Homotopy Type Theory


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


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

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

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


Its induction principle? says that for any P:S 1TypeP:S^1\to Type equipped with a point base:P(base)base' : P(base) and a dependent path? loop:base=baseloop':base'= base', there is f: (x:S 1)P(x)f:\prod_{(x:S^1)} P(x) such that:

f(base)=baseapd f(loop)=loopf(base)=base'\qquad apd_f(loop) = loop'

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

f(base)=xap f(loop)=lf(base)=x\qquad ap_f(loop)=l

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

There are several proofs in the book that the loop space Ω(S 1)\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 1S^1 is contractible. Indeed, S 1S^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.

See also


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.