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.
Let denote the identification type between elements and of type , and let denote the heterogeneous identification type between elements and of type family , given elements and and identification . Let denote the dependent function application of the dependent function to the identification
In the natural deduction formulation of dependent type theory, the circle type is given by the following inference rules:
Formation rules for the circle type:
Introduction rules for the circle type:
Elimination rules for the circle type:
Computation rules for the circle type:
Uniqueness rules for the circle type:
The elimination, computation, and uniqueness rules for the circle type state that the circle type satisfy the dependent universal property of the circle type. If the dependent type theory also has dependent sum types and product types, allowing one to define the uniqueness quantifier, the dependent universal property of the circle type could be simplified to the following rule:
The circle type could also be defined as the suspension type of the type of booleans .
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 -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
equipped with a point
and a dependent path ,
there is such that:
As a special case, its recursion principle says that given any type with a point and a loop , there is with
The extensionality principle of the circle type says that there is an equivalence of types between the identification type and the type of integers :
Equivalently, that the loop space type is equivalent to the integers.
Thus, the extensionality principle of the circle type implies that the integers and thus the natural numbers are contractible types if axiom K or uniqueness of identity proofs hold for the entire type theory. If the extensionality principle of the natural numbers also hold in the type theory, then every type is contractible.
One could prove the extensionality principle of the circle type, given a univalent universe where the circle is small relative to the universe. The HoTT book provides a number of such proofs.
The type of H-spaces on the circle type is a contractible type.
lemniscate type?
The formalization of the shape homotopy type of the circle as a higher inductive type in homotopy type theory, along with a proof that (and hence ):
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 -torsors:
Alternative construction of the circle type as a coequalizer:
For the fact that the type of H-space structures on a circle type is contractible:
Last revised on August 2, 2023 at 12:44:13. See the history of this page for a list of all contributions to it.