# Homotopy Type Theory HoTT book real numbers > history (changes)

Showing changes from revision #12 to #13: Added | Removed | Changed

# Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

## Definition

### In set theory

Let $F$ be an Archimedean ordered field and let

$F_{+} \coloneqq \sum_{a:F} 0 \lt a$

be the positive elements in $F$. $F$ is sequentially Cauchy complete if every Cauchy sequence in $F$ converges:

$isCauchy(x) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (\vert x_i - x_j \vert \lt \epsilon)$
$isLimit(x, l) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon)$
$\forall x \in F^\mathbb{N}. isCauchy(x) \wedge \exists l \in F. isLimit(x, l)$

The set of HoTT book real numbers $\mathbb{R}_H$ is the initial sequentially Cauchy complete? Archimedean ordered field.

The set of HoTT book real numbers $\mathbb{R}_H$ is the initial object in the category of Cauchy structures and Cauchy structure homomorphisms.

### In homotopy type theory

The HoTT book real numbers $\mathbb{R}_H$ are a homotopy initial Cauchy structure, i.e. a Cauchy structure such that for every other Cauchy structure $S$, the type of Cauchy structure homomorphisms with domain $\mathbb{R}_H$ and codomain $S$ is contractible.

#### As a higher inductive-inductive type

Let $\mathbb{Q}$ be the rational numbers and let

$\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x$

be the positive rational numbers. The HoTT book real numbers $\mathbb{R}_H$ are inductively generated by the following:

• a function $inj: \mathbb{Q} \to \mathbb{R}_H$

• a function $lim: C(\mathbb{R}_H) \to \mathbb{R}_H$, where $C(\mathbb{R}_H)$ is the type of Cauchy approximations in $\mathbb{R}_H$.

• a dependent family of terms

$a:\mathbb{R}_H, b:\mathbb{R}_H \vdash eq_{\mathbb{R}_H}(a, b): \left( \prod_{\epsilon:\mathbb{Q}_{+}} (a \sim_{\epsilon} b) \right) \to (a =_{\mathbb{R}_H} b)$

and the premetric type family $\sim$ is simultaneously inductively generated by the following:

• a dependent family of terms

$a:\mathbb{Q}, b:\mathbb{Q}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, \mathbb{Q}}(a, b, \epsilon): (\vert a - b \vert \lt \epsilon) \to (inj(a) \sim_{\epsilon} inj(b))$
• a dependent family of terms

$a:\mathbb{Q}, b:C(\mathbb{R}_H), \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, C(\mathbb{R}_H)}(a, b, \epsilon, \eta): (inj(a) \sim_{\epsilon} b_{\eta}) \to (inj(a) \sim_{\epsilon + \eta} lim(b))$
• a dependent family of terms

$a:C(\mathbb{R}_H), b:\mathbb{Q}, \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{C(\mathbb{R}_H), \mathbb{Q}}(a, b, \delta, \epsilon): (a_{\delta} \sim_{\epsilon} inj(b) ) \to (lim(a) \sim_{\delta + \epsilon} inj(b))$
• a dependent family of terms

$a:C(\mathbb{R}_H), b:C(\mathbb{R}_H), \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{C(\mathbb{R}_H), C(\mathbb{R}_H)}(a, b, \delta, \epsilon, \eta): (a_{\delta} \sim_{\epsilon} b_{\eta} ) \to (lim(a) \sim_{\delta + \epsilon + \eta} lim(b))$
• a dependent family of terms

$a:\mathbb{Q}, b:\mathbb{Q}, \epsilon:\mathbb{Q}_{+} \vdash \pi(a, b, \epsilon): isProp(a \sim_{\epsilon} b)$