natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The circle type is an axiomatization of the homotopy type of the (shape of) the circle in the context of homotopy type theory.
As a higher inductive type, the circle is given by
Inductive Circle : Type
| base : Circle
| loop : Id Circle base base
This says that the type is inductively constructed from
a term of circle type whose interpretation is as the base point of the circle,
a term of the identity type of paths between these two terms, which interprets as the 1-cell of the circle
Hence a non-constant path from the base point to itself.
The circle type could also be defined as the suspension type $\Sigma \mathbf{2}$ of the type of booleans $\mathbf{2}$.
The circle type could also be defined as the coequalizer type of any two endofunctions on the unit type
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.
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:
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
There are several proofs in the HoTT 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 definition of the circle type as a coequalizer could be found in section 9 of
A formalization of the shape homotopy type $ʃ S^1 \simeq \mathbf{B}\mathbb{Z}$ of the circle as a higher inductive type in homotopy type theory, along with a proof that $\Omega ʃS^1\simeq {\mathbb{Z}}$ (and hence $\pi_1(ʃS^1) \simeq \mathbb{Z}$):
Dan Licata, Mike Shulman, Calculating the Fundamental Group of the Circle in Homotopy Type Theory, LICS ‘13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science June 2013 (arXiv:1301.3443, doi:10.1109/LICS.2013.28)
blog announcements:
Marc Bezem, Ulrik Buchholtz, Daniel Grayson, Michael Shulman, Construction of the Circle in UniMath, Journal of Pure and Applied Algebra Volume 225, Issue 10, October 2021, 106687 (arXiv:1910.01856)
The proof is formalized therein using the Agda proof assistant. See also
The HoTT Book, section 8.1
The HoTT Coq library: theories/hit/Circle.v
The HoTT Agda library: homotopy/LoopSpaceCircle.agda
Last revised on October 22, 2022 at 22:23:56. See the history of this page for a list of all contributions to it.