Homotopy Type Theory
circle (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

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

This page is under construction. - Ali

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

Idea

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.

Definition

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

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

See also

higher inductive type

References

HoTT book


Old Page

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.

Properties

Ω(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

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.

category: homotopy theory

Revision on September 5, 2018 at 17:01:04 by Ali Caglayan. See the history of this page for a list of all contributions to it.