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
Similar to how the interval type is the abstract homotopy type for the unit interval and the circle type is the abstract homotopy type for the unit circle, the line type is the abstract homotopy type for the real line.
The line type $A^1$ is the higher inductive type generated by
an element $0:A^1$
an equivalence of types $s:A^1 \simeq A^1$
an identification $p:0 =_{A^1} s(0)$
Equivalently, it is the higher inductive type generated by
an element $0:A^1$
an equivalence of types $s:A^1 \simeq A^1$
for each $x:A^1$, an identification $p(x):x =_{A^1} s(x)$
Equivalently, it is the higher inductive type generated by
a function $c:\mathbb{Z} \to A^1$
for each $z:\mathbb{Z}$, an identification $p(z):c(z) =_{A^1} c(s(z))$
where $\mathbb{Z}$ is the integers type.
The line type is contractible; see section 8.1.5 of UFP13.
The line type is equivalent to the propositional truncation of the integers type.
The circle type $S^1$ is the coequalizer type of the pair of functions on the line type
This is the analogue in synthetic homotopy theory of the fact that the unit circle is the coequalizer of the pair of functions on the real line in classical homotopy theory:
In real-cohesive homotopy type theory, the shape of the real numbers is equivalent to the line type $\esh(\mathbb{R}) \simeq A^1$.
The line type is defined as “homotopical reals” in section 8.1.5 of
Last revised on November 11, 2023 at 13:17:26. See the history of this page for a list of all contributions to it.