## Idea ## The circle is one of the simplest [[higher inductive types]] it consists of a single point and a single non-trivial path between. ## Definition ## The **circle** denoted $S^1$ is defined as the [[higher inductive type]] generated by: * A point $base : S^1$ * A [[path]] $loop : base = base$ Alternative definitions include the [[suspension]] of $\mathbf{2}$ and as a [[coequalizer]]. ## Properties ## 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'= base'$, there is $f:\prod_{(x:S^1)} P(x)$ such that: $$f(base)=base'\qquad 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\qquad ap_f(loop)=l$$ ### $\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]]. ## See also ## * [[higher inductive type]] * [[homotopy groups of spheres]] ## References ## [[HoTT book]] [[!redirects S^1]] [[!redirects S¹]] category: homotopy theory