nLab line type

 Idea

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.

Definition

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.

 Properties

The line type is contractible; see section 8.1.5 of UFP13.

Relation to the integers

The line type is equivalent to the propositional truncation of the integers type.

Relation to the circle type

The circle type $S^1$ is the coequalizer type of the pair of functions on the line type

$$A^1\underoverset{\quad s \quad}{\mathrm{id}_{A^1}}{\rightrightarrows}A^1 \to S^1$$

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:

$$\mathbb{R} \underoverset{\quad (-) + 1 \quad}{\mathrm{id}_\mathbb{R}}{\rightrightarrows}\mathbb{R} \to \mathbb{S}^1$$

 Relation to the real numbers

In real-cohesive homotopy type theory, the shape of the real numbers is equivalent to the line type $\esh(\mathbb{R}) \simeq A^1$.

Related concepts

• real numbers

• integers type

• interval type

• circle type

References

The line type is defined as “homotopical reals” in section 8.1.5 of

• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Project, Institute for Advanced Study, 2013. (web, pdf)