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

The circle$S^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^1$, and

a path $loop:base=base$.

Idea

Its induction principle? says that for any $P:S^1\to Type$ equipped with a point $base^* : P(base)$ and a dependent path?$loop^*:base^*=_{loop} base^*$, there is $f:\prod_{(x:S^1)} P(x)$ such that $f(base)=base^*$ and $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$ and $f(loop)=l$.

Definition

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

There are several proofs in the 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.)

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

a point $base:S^1$, and

a path $loop:base=base$.

Its induction principle? says that for any $P:S^1\to Type$ equipped with a point $base^* : P(base)$ and a dependent path?$loop^*:base^*=_{loop} base^*$, there is $f:\prod_{(x:S^1)} P(x)$ such that $f(base)=base^*$ and $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$ and $f(loop)=l$.

Properties

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

There are several proofs in the 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.)

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.