# Contents

## 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$.

## References

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.