Contents

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

Definition

Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$. The HoTT book real numbers $\mathbb{R}_H$ are a homotopy initial $R_{+}$-Cauchy structure, i.e. an $R_{+}$-Cauchy structure such that for every other $R_{+}$-Cauchy structure $S$, the type of $R_{+}$-Cauchy structure homomorphisms with domain $\mathbb{R}_H$ and codomain $S$ is contractible.

As a higher inductive-inductive type

Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$. The HoTT book real numbers $\mathbb{R}_H$ are inductively generated by the following:

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

• a function $lim: C(\mathbb{R}_H, R_{+}) \to \mathbb{R}_H$, where $C(\mathbb{R}_H, R_{+})$ is the type of $R_{+}$-indexed nets in $\mathbb{R}_H$ that are $R_{+}$-Cauchy approximations.

• a dependent family of terms

and the $R_{+}$-premetric type family $\sim$ is simultaneously inductively generated by the following:

• a dependent family of terms

  $$a:R, b:R, \epsilon:R_{+} \vdash \mu_{R, R}(a, b, \epsilon): (\vert a - b \vert \lt \epsilon) \to (inj(a) \sim_{\epsilon} inj(b))$$

• a dependent family of terms

  $$a:R, b:C(\mathbb{R}_H, R_{+}), \epsilon:R_{+}, \eta:R_{+} \vdash \mu_{R, C(\mathbb{R}_H, R_{+})}(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, R_{+}), b:R, \delta:R_{+}, \epsilon:R_{+} \vdash \mu_{C(\mathbb{R}_H, R_{+}), R}(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, R_{+}), b:C(\mathbb{R}_H, R_{+}), \delta:R_{+}, \epsilon:R_{+}, \eta:R_{+} \vdash \mu_{C(\mathbb{R}_H, R_{+}), C(\mathbb{R}_H, R_{+})}(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:R, b:R, \epsilon:R_{+} \vdash \pi(a, b, \epsilon): isProp(a \sim_{\epsilon} b)$$

In set theory

A premetric space is a set $S$ with a ternary relation $\sim$ on the Cartesian product $\mathbb{Q}_{+} \times S \times S$, where

is the set of positive rational numbers. A Cauchy approximation in $S$ is an function $x \in S^{\mathbb{Q}_{+}}$, where $S^{\mathbb{Q}_{+}}$ is the set of functions with domain $\mathbb{Q}_{+}$ and codomain $S$, such that

The set of all Cauchy approximations is defined as

A Cauchy structure is a premetric space $S$ with a function $rat \in S^{\mathbb{Q}_{+}}$ and a function $lim \in S^{C(S)}$ such that

For two Cauchy structures $S$ and $T$, a Cauchy structure homomorphism is a function $f\in T^S$ such that

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

See also

• Cauchy real numbers
• generalized Cauchy real numbers
• Cauchy real numbers (disambiguation)
• premetric space

References

• Auke B. Booij, Analysis in univalent type theory (pdf)
• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)