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 (e.g. UFP13, p. 177) that for
any $P \colon S^1 \to Type$
equipped with a point $base' \colon P(base)$
and a dependent path $loop' \,\colon\, base' =_{loop} 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.)
lemniscate type?
The 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:
Formalization in proof assistants:
in Coq:
in Agda:
Exposition and review:
Alternative construction of the circle type as the type of $\mathbb{Z}$-torsors:
Alternative construction of the circle type as a coequalizer:
Last revised on March 2, 2023 at 05:25:52. See the history of this page for a list of all contributions to it.