Homotopy Type Theory modulated Cauchy real numbers > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Definition

Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$ . Let As us a define result,$R$ is a directed type and a codirected type where the directed type operation $+$ is associative.

The Cauchy real numbers $\mathbb{R}_C$ are inductively generated by the following:

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

• a dependent family of terms

  $$a:C(R, R_{+}), b:C(R, R_{+}) \vdash eq_{\mathbb{R}_C}(a, b): \left( \prod_{\epsilon:R_{+}} a_\epsilon \sim_{\epsilon} b \right) \to (inj(a) =_{\mathbb{R}_C} inj(b))$$

  where the $R_{+}$-premetric for $\epsilon:R_{+}$ is defined as

  $$a \sim_{\epsilon} b \coloneqq \vert a_\epsilon - b_\epsilon \vert \lt 4 \epsilon$$

• a family of dependent terms

  $$a:\mathbb{R}_C, b:\mathbb{R}_C \vdash \tau(a, b): isProp(a =_{\mathbb{R}_C} b)$$

The Cauchy real numbers are sometimes defined using sequences $x:\mathbb{N} \to R$, $y:\mathbb{N} \to R$ with modulus of Cauchy convergence $M:R_{+} \to \mathbb{N}$, $N:R_{+} \to \mathbb{N}$ respectively. However, the composition of a sequence and a modulus of Cauchy convergence yields a Cauchy approximation, so one could define Cauchy approximations $a:R_{+} \to R$ as $a \coloneqq x \circ M$ and $b:R_{+} \to R$ as $b \coloneqq y \circ N$, with $x_{M(\epsilon)} = a_\epsilon$ and $y_{N(\epsilon)} = b_\epsilon$ following from function evaluation. In fact, Cauchy approximations and sequences with a modulus of Cauchy convergence are inter-definable.

See also

• Cauchy real numbers (disambiguation)
• HoTT book real numbers
• premetric space
• infinite decimal representation of the Cauchy real numbers?

References

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