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 inductive constructed from a terms in the circle, whose interpretation is as the base point of the circle, together with a term in the identity type of paths between these two terms, which interprets as the 1-cell of the circle
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}$.
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 announcement: A formal proof that $\pi_1(S^1) = \mathbb{Z}$
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 July 12, 2021 at 14:33:23. See the history of this page for a list of all contributions to it.