Equivalence of Cauchy Sequences and Cauchy Approximations, HoTT

Question

In HoTT book (Homotopy Type Theory), in order to construct Cauchy reals they introduce the notion of Cauchy approximation, which are defined as :

$$x \hspace{0.1cm} \colon \mathbb{Q} \to \mathbb{R} \hspace{0.1cm} \mbox{such that} \hspace{0.1cm} \forall \hspace{0.1cm} (\epsilon, \delta \colon \mathbb{Q}_+). d(x_{\epsilon}-x_{\delta})< \epsilon + \delta$$

If I have a standard Cauchy sequence $x \hspace{0.1cm} \colon \mathbb{N} \to \mathbb{R}$ than I can obtain a Cauchy approximation via its modulus of convergence $M$, i.e. the function $\epsilon \to x_{M(\epsilon)}$.

On the other hand, if I have a Cauchy approximation I can get a Cauchy sequence for example by $n \to x_{\frac{1}{n}}$.

My question is : how do I show (if it's possible) that these two notions are equivalent if I'm interested only in their limits? More precisely :

• if I have a Cauchy approximation $x$ and two Cauchy sequences $\bar{x}, \tilde{x}$ obtained from $x$, is it true that $\mbox{lim}(\bar{x})= \mbox{lim}( \tilde{x})$ ?
• if I have a Cauchy sequence $x$ and two Cauchy approximations $\bar{x}, \tilde{x}$ obtained from $x$, do they have the same limit?

I think it would be sufficient to show that in either cases they are arbitrarily close.

Any help would be appreciated!

Answer 1

It depends on exactly what you mean by "obtained from", so let me make that definite:

• If $x$ is a Cauchy approximation, and $\epsilon_n,\delta_n : \Bbb N \to \Bbb Q_+$ are two sequences such that $\epsilon_n \to 0, \delta_n \to 0$ as $n \to \infty$, then $$\lim_{n\to\infty} x(\epsilon_n) = \lim_{n \to \infty} x(\delta_n) = \lim_{\epsilon \to 0+} x(\epsilon)$$
• If $y$ is a Cauchy sequence, and $n, m : \Bbb Q_+ \to \Bbb N$ are two functions such that $\lim_{\epsilon \to 0+}n(\epsilon) = \infty$ and $\lim_{\epsilon \to 0+}m(\epsilon) = \infty$, then $$\lim_{\epsilon \to 0+}y_{n(\epsilon)} = \lim_{\epsilon \to 0+}y_{m(\epsilon)} = \lim_{n \to \infty}y_n$$

(I am assuming $0\notin \Bbb Q_+$. If you are allowing $0 \in \Bbb Q_+$ then certain adjustments must be made in this post.)

Both of these follow from the fact that Cauchy sequences and approximations in $\Bbb R$ always converge, and a more general result about limits:

If $X, Y, Z$ are topological spaces with maps (not necessarily continuous) $g: X \to Y, f: Y \to Z$ and $x_0 \in X, y_0 \in Y, z_0 \in Z$ such that

1. $g(x) \ne y_0$ in some deleted neighborhood of $x_0$,
2. $\lim_{x \to x_0} g(x) = y_0$,
3. $\lim_{y \to y_0} f(y) = z_0$, then $$\lim_{x\to x_0} f(g(x)) = z_0$$

This is not hard to prove: if $W$ is a neighborhood of $z_0$, then because $\lim_{y \to y_0} f(y) = z_0$, there is a deleted neighborhood $V$ of $y_0$ with $f(V) \subset W$, and because $\lim_{x \to x_0} g(x) = y_0$ there is a deleted neighborhood $U$ of $x_0$ with $g(U) \subset V\cup{y_0}$, and by the first condition another deleted neighborhood $T$ of $x_0$ with $g(x) \ne y_0$ for all $x \in T$. Therefore $U\cap T$ is a deleted neighborhood of $x_0$ with $f\circ g(U\cap T) \subset W$. Since $W$ was arbitrary, $$\lim_{x\to x_0} f(g(x)) = z_0$$