+--{.query} *This page is under construction. - Ali* =-- ## Idea ## ## Definition ## ## Properties ## ## See also ## [[higher inductive type]] ## References ## [[HoTT book]] *** # Old Page # 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.) Two of them were blogged about: * The [first proof](http://homotopytypetheory.org/2011/04/29/a-formal-proof-that-pi1s1-is-z/) by [[Mike Shulman]] * A [simplification](http://homotopytypetheory.org/2012/06/07/a-simpler-proof-that-%cf%80%e2%82%81s%c2%b9-is-z/) by [[Dan Licata]] ### 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]]. [[!redirects S^1]] [[!redirects S¹]] category: homotopy theory