Sequential colimit of iterated quotients of Cauchy sequences

Question

We work in constructive mathematics.

The sets and functions in the foundations form a Grothendieck topos, which means that all colimits exist, and in particular, that all sequential colimits exist. Given a sequence of sets $A_n$ and a sequence of functions $f_n:A_n \to A_{n + 1}$, the sequential colimit of the diagram

$$A_0 \overset{f_0}\to A_1 \overset{f_1}\to A_2 \overset{f_2}\to \ldots$$

is the set $A_\infty$ with a sequence of functions $i_n:A_n \to A_\infty$ where $i_{n + 1}(f_{n}(e)) = i_{n}(e)$ for all elements $e \in A_n$, such that for any other set $B$ and sequence of functions $j_n:A_n \to B$ where $j_{n + 1}(f_{n}(e)) = j_{n}(e)$ for all elements $e \in A_n$, there is a unique function $u_B:A_\infty \to B$ such that for all natural numbers $n$ and for all elemenets $e \in A_n$, $u_B(i_n(e)) = j_n(e)$.

Let $F$ be an Archimedean ordered field. $F$ is Cauchy complete if every Cauchy sequence in $F$ converges.

Now, let us begin with the set of rational numbers $\mathbb{Q}$. By taking the quotient set of equivalent Cauchy sequences of rational numbers, one gets the Cauchy real numbers $\mathbb{R}_C$ with a unique injective field homomorphism $\mathbb{Q} \hookrightarrow \mathbb{R}_C$. The Cauchy real numbers, constructed in this manner, cannot be proven to be Cauchy complete in constructive mathematics, however.

Now, instead of the rational numbers $\mathbb{Q}$, one could take any Archimedean ordered field $F$, and perform the same construction as above: by taking the quotient set of equivalent Cauchy sequences of elements of $F$, one gets another Archimedean ordered field which is denoted here as $\mathrm{QuotCauchy}(F)$, with a unique injective field homomorphism $F \hookrightarrow \mathrm{QuotCauchy}(F)$. If $F$ is already Cauchy complete, then the field homomorphism is a field isomorphism, but this usually cannot be proven for arbitrary Archimedean ordered fields $F$ in constructive mathematics.

This implies that one could repeatedly construct the quotient set of Cauchy sequences starting from the rational numbers, yielding a sequence of unique injective field homomorphisms between Archimedean ordered fields

$$\mathbb{Q} \hookrightarrow \mathrm{QuotCauchy}(\mathbb{Q}) \hookrightarrow \mathrm{QuotCauchy}^2(\mathbb{Q}) = \mathrm{QuotCauchy}(\mathrm{QuotCauchy}(\mathbb{Q})) \hookrightarrow \ldots$$

Is the sequential colimit of this diagram above a Cauchy complete Archimedean ordered field? If it is, is it the initial Cauchy complete Archimedean ordered field?

Answer 1

$\mathrm{QuotCauchy}$ defined above is an endofunctor on the category of Archimedean ordered fields. Thus, the question above is tantamount to asking whether the sequential limit $\mathrm{QuotCauchy}^\infty(\mathbb{Q})$ is the initial $\mathrm{QuotCauchy}$-algebra.

Mike Shulman on the HoTT Zulipchat says:

Yes, it is frequently the case that you can construct an initial $F$-algebra for an endofunctor $F$ by iterating $F$ on the empty set, or more generally the free $F$-algebra on a type $A$ by iterating $F$ on $A$, but this only works when $F$ preserves sequential colimits, so that $$F(F^\infty(A)) = F(\mathrm{colim}_n F^n(A)) = \mathrm{colim}_n F(F^n(A)) = \mathrm{colim}_n F^{n+1}(A) = F^\infty(A).$$ This is the case for $F(X)=X+1$, so you can construct the natural numbers this way. But it's not the case for $F = \mathrm{QuotCauchy}$, essentially because the definition of $\mathrm{QuotCauchy}$ involves infinite sequences of elements. That is, if you have a sequential colimit diagram $X_0 \to X_1 \to X_2 \to\cdots$ with colimit $X_\infty$, then you could have an element of $\mathrm{QuotCauchy}(X_\infty)$ arising from a sequence $(x_n)$ for which (informally) $x_n \in X_n\setminus X_{n-1}$, and then that element of $\mathrm{QuotCauchy}(X_\infty)$ won't have a limit in $X_\infty$.

In the same thread, David Warn writes:

Just to give a perhaps more down-to-earth explanation of what's going on here: let's suppose we have an ambient Cauchy complete extension of $\mathbb Q$ like the Dedekind or HoTT book reals, written $\mathbb R$. Given a subset $X$ of $\mathbb R$, we can consider the subset $FX$ of $\mathbb R$ consisting of limits of Cauchy sequences of elements of $X$. I believe this is compatible with the $F$ defined above, but this way it's perhaps easier to understand the limit, where we consider the subset $F^\infty X := \bigcup_{n=0}^\infty F^n X$ of $\mathbb R$. OK, how would we show that $F^\infty X$ is Cauchy complete? Say we have a Cauchy sequence $x_n$ in $F^\infty X$. For each $n$, we know there merely exists $i$ such that $x_n \in F^i X$. But in the absence of countable choice, it seems hopeless to look for a choice of $i$ for each $n$. This is our first problem. The second, equally severe problem is that even given a choice of $i_n$ for each $n$, it can happen that the sequence $i_n$ is unbounded. We still have to produce a single $N$ such that the limit $x_n$ is in $F^N X$, which seems hopeless.

So taking the sequential limit of the diagram $$\mathbb{Q} \hookrightarrow \mathrm{QuotCauchy}(\mathbb{Q}) \hookrightarrow \mathrm{QuotCauchy}^2(\mathbb{Q}) = \mathrm{QuotCauchy}(\mathrm{QuotCauchy}(\mathbb{Q})) \hookrightarrow \ldots$$ is not sufficient to get Cauchy completion.