Homotopy Type Theory
circle (Rev #1, changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

The circle S 1S^1 is most commonly defined in homotopy type theory as a higher inductive type generated by

  • a point base:S 1base:S^1, and
  • a path loop:base=baseloop:base=base.

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 *= loopbase *loop^*:base^*=_{loop} base^*, there is f: (x:S 1)P(x)f:\prod_{(x:S^1)} P(x) such that f(base)=base *f(base)=base^* and apd f(loop)=loop *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)=xf(base)=x and f(loop)=lf(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.

Revision on May 15, 2014 at 08:38:29 by Mike Shulman. See the history of this page for a list of all contributions to it.