# 11.3.2 Induction and recursion on Cauchy reals

In order to do anything useful with $\mathbb{R}_{\mathsf{c}}$, of course, we need to give its induction principle. As is the case whenever we inductively define two or more objects at once, the basic induction principle for $\mathbb{R}_{\mathsf{c}}$ and $\mathord{\sim}$ requires a simultaneous induction over both at once. Thus, we should expect it to say that assuming two type families over $\mathbb{R}_{\mathsf{c}}$ and $\mathord{\sim}$, respectively, together with data corresponding to each constructor, there exist sections of both of these families. However, since $\mathord{\sim}$ is indexed on two copies of $\mathbb{R}_{\mathsf{c}}$, the precise dependencies of these families is a bit subtle. The induction principle will apply to any pair of type families:

 $\displaystyle A$ $\displaystyle:\mathbb{R}_{\mathsf{c}}\to\mathcal{U}$ $\displaystyle B$ $\displaystyle:\mathchoice{\prod_{x,y:\mathbb{R}_{\mathsf{c}}}\,}{\mathchoice{{% \textstyle\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}}{\prod_{(x,y:\mathbb{R}_{% \mathsf{c}})}}{\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x,y:\mathbb{R}_{% \mathsf{c}})}}}{\mathchoice{{\textstyle\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}}% {\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}% {\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}}{\mathchoice{{\textstyle\prod_{(x,y:% \mathbb{R}_{\mathsf{c}})}}}{\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x,y% :\mathbb{R}_{\mathsf{c}})}}{\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}}A(x)\to A(y% )\to\mathchoice{\prod_{\epsilon:\mathbb{Q}_{+}}\,}{\mathchoice{{\textstyle% \prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{% (\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\mathchoice{{% \textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})% }}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{% \mathchoice{{\textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:% \mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{% Q}_{+})}}}(x\sim_{\epsilon}y)\to\mathcal{U}.$

The type of $A$ is obvious, but the type of $B$ requires a little thought. Since $B$ must depend on $\mathord{\sim}$, but $\mathord{\sim}$ in turn depends on two copies of $\mathbb{R}_{\mathsf{c}}$ and one copy of $\mathbb{Q}_{+}$, it is fairly obvious that $B$ must also depend on the variables $x,y:\mathbb{R}_{\mathsf{c}}$ and $\epsilon:\mathbb{Q}_{+}$ as well as an element of $(x\sim_{\epsilon}y)$. What is slightly less obvious is that $B$ must also depend on $A(x)$ and $A(y)$.

This may be more evident if we consider the non-dependent case (the recursion principle), where $A$ is a simple type (rather than a type family). In this case we would expect $B$ not to depend on $x,y:\mathbb{R}_{\mathsf{c}}$ or $x\sim_{\epsilon}y$. But the recursion principle (along with its associated uniqueness principle) is supposed to say that $\mathbb{R}_{\mathsf{c}}$ with $\sim_{\epsilon}$ is an βinitial objectβ in some category, so in this case the dependency structure of $A$ and $B$ should mirror that of $\mathbb{R}_{\mathsf{c}}$ and $\sim_{\epsilon}$: that is, we should have $B:A\to A\to\mathbb{Q}_{+}\to\mathcal{U}$. Combining this observation with the fact that, in the dependent case, $B$ must also depend on $x,y:\mathbb{R}_{\mathsf{c}}$ and $x\sim_{\epsilon}y$, leads inevitably to the type given above for $B$.

It is helpful to think of $B$ as an $\epsilon$-indexed family of relations between the types $A(x)$ and $A(y)$. With this in mind, we may write $B(x,y,a,b,\epsilon,\xi)$ as $(x,a)\frown_{\epsilon}^{\xi}(y,b)$. Since $\xi:x\sim_{\epsilon}y$ is unique when it exists, we generally omit it from the notation and write $(x,a)\frown_{\epsilon}(y,b)$; this is harmless as long as we keep in mind that this relation is only defined when $x\sim_{\epsilon}y$. We may also sometimes simplify further and write $a\frown_{\epsilon}b$, with $x$ and $y$ inferred from the types of $a$ and $b$, but sometimes it will be necessary to include them for clarity.

Now, given a type family $A:\mathbb{R}_{\mathsf{c}}\to\mathcal{U}$ and a family of relations $\frown$ as above, the hypotheses of the induction principle consist of the following data, one for each constructor of $\mathbb{R}_{\mathsf{c}}$ or $\mathord{\sim}$:

• β’

For any $q:\mathbb{Q}$, an element $f_{q}:A(\mathsf{rat}(q))$.

• β’

For any Cauchy approximation $x$, and any $a:\mathchoice{\prod_{\epsilon:\mathbb{Q}_{+}}\,}{\mathchoice{{\textstyle\prod_% {(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(% \epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\mathchoice{{% \textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})% }}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{% \mathchoice{{\textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:% \mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{% Q}_{+})}}}A(x_{\epsilon})$ such that

 $\forall(\delta,\epsilon:\mathbb{Q}_{+}).\,(x_{\delta},a_{\delta})\frown_{% \delta+\epsilon}(x_{\epsilon},a_{\epsilon}),$ (11.3.1)

an element $f_{x,a}:A(\mathsf{lim}(x))$. We call such $a$ a dependent Cauchy approximation over $x$.

• β’

For $u,v:\mathbb{R}_{\mathsf{c}}$ such that $h:\forall(\epsilon:\mathbb{Q}_{+}).\,u\sim_{\epsilon}v$, and all $a:A(u)$ and $b:A(v)$ such that $\forall(\epsilon:\mathbb{Q}_{+}).\,(u,a)\frown_{\epsilon}(v,b)$, a dependent path $a=^{A}_{\mathsf{eq}_{\mathbb{R}_{\mathsf{c}}}(u,v)}b$.

• β’

For $q,r:\mathbb{Q}$ and $\epsilon:\mathbb{Q}_{+}$, if $-\epsilon, we have $(\mathsf{rat}(q),f_{q})\frown_{\epsilon}(\mathsf{rat}(r),f_{r}).$

• β’

For $q:\mathbb{Q}$ and $\delta,\epsilon:\mathbb{Q}_{+}$ and $y$ a Cauchy approximation, and $b$ a dependent Cauchy approximation over $y$, if $\mathsf{rat}(q)\sim_{\epsilon-\delta}y_{\delta}$, then

 $(\mathsf{rat}(q),f_{q})\frown_{\epsilon-\delta}(y_{\delta},b_{\delta})\;% \Rightarrow\;(\mathsf{rat}(q),f_{q})\frown_{\epsilon}(\mathsf{lim}(y),f_{y,b}).$
• β’

Similarly, for $r:\mathbb{Q}$ and $\delta,\epsilon:\mathbb{Q}_{+}$ and $x$ a Cauchy approximation, and $a$ a dependent Cauchy approximation over $x$, if $x_{\delta}\sim_{\epsilon-\delta}\mathsf{rat}(r)$, then

 $(x_{\delta},a_{\delta})\frown_{\epsilon-\delta}(\mathsf{rat}(r),f_{r})\;% \Rightarrow\;(\mathsf{lim}(x),f_{x,a})\frown_{\epsilon}(\mathsf{rat}(q),f_{r}).$
• β’

For $\epsilon,\delta,\eta:\mathbb{Q}_{+}$ and $x,y$ Cauchy approximations, and $a$ and $b$ dependent Cauchy approximations over $x$ and $y$ respectively, if we have $x_{\delta}\sim_{\epsilon-\delta-\eta}y_{\eta}$, then

 $(x_{\delta},a_{\delta})\frown_{\epsilon-\delta-\eta}(y_{\eta},b_{\eta})\;% \Rightarrow\;(\mathsf{lim}(x),f_{x,a})\frown_{\epsilon}(\mathsf{lim}(y),f_{y,b% }).$
• β’

For $\epsilon:\mathbb{Q}_{+}$ and $x,y:\mathbb{R}_{\mathsf{c}}$ and $\xi,\zeta:x\sim_{\epsilon}y$, and $a:A(x)$ and $b:A(y)$, any two elements of $(x,a)\frown_{\epsilon}^{\xi}(y,b)$ and $(x,a)\frown_{\epsilon}^{\zeta}(y,b)$ are dependently equal over $\xi=\zeta$. Note that as usual, this is equivalent to asking that $\frown$ takes values in mere propositions.

Under these hypotheses, we deduce functions

 $\displaystyle f$ $\displaystyle:\mathchoice{\prod_{x:\mathbb{R}_{\mathsf{c}}}\,}{\mathchoice{{% \textstyle\prod_{(x:\mathbb{R}_{\mathsf{c}})}}}{\prod_{(x:\mathbb{R}_{\mathsf{% c}})}}{\prod_{(x:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x:\mathbb{R}_{\mathsf{c}})% }}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R}_{\mathsf{c}})}}}{\prod_{(x:% \mathbb{R}_{\mathsf{c}})}}{\prod_{(x:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x:% \mathbb{R}_{\mathsf{c}})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R}_{% \mathsf{c}})}}}{\prod_{(x:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x:\mathbb{R}_{% \mathsf{c}})}}{\prod_{(x:\mathbb{R}_{\mathsf{c}})}}}A(x)$ $\displaystyle g$ $\displaystyle:\mathchoice{\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}\,}{\mathchoice% {{\textstyle\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}}{\prod_{(x,y:\mathbb{R}_{% \mathsf{c}})}}{\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x,y:\mathbb{R}_{% \mathsf{c}})}}}{\mathchoice{{\textstyle\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}}% {\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}% {\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}}{\mathchoice{{\textstyle\prod_{(x,y:% \mathbb{R}_{\mathsf{c}})}}}{\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x,y% :\mathbb{R}_{\mathsf{c}})}}{\prod_{(x,y:\mathbb{R}_{\mathsf{c}})}}}\mathchoice% {\prod_{(\epsilon:\mathbb{Q}_{+})}\,}{\mathchoice{{\textstyle\prod_{(\epsilon:% \mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb% {Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\mathchoice{{\textstyle\prod_{(% \epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(% \epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\mathchoice{{% \textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})% }}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}% \mathchoice{\prod_{(\xi:x\sim_{\epsilon}y)}\,}{\mathchoice{{\textstyle\prod_{(% \xi:x\sim_{\epsilon}y)}}}{\prod_{(\xi:x\sim_{\epsilon}y)}}{\prod_{(\xi:x\sim_{% \epsilon}y)}}{\prod_{(\xi:x\sim_{\epsilon}y)}}}{\mathchoice{{\textstyle\prod_{% (\xi:x\sim_{\epsilon}y)}}}{\prod_{(\xi:x\sim_{\epsilon}y)}}{\prod_{(\xi:x\sim_% {\epsilon}y)}}{\prod_{(\xi:x\sim_{\epsilon}y)}}}{\mathchoice{{\textstyle\prod_% {(\xi:x\sim_{\epsilon}y)}}}{\prod_{(\xi:x\sim_{\epsilon}y)}}{\prod_{(\xi:x\sim% _{\epsilon}y)}}{\prod_{(\xi:x\sim_{\epsilon}y)}}}(x,f(x))\frown_{\epsilon}^{% \xi}(y,f(y))$

which compute as expected:

 $\displaystyle f(\mathsf{rat}(q))$ $\displaystyle:\!\!\equiv f_{q},$ (11.3.2) $\displaystyle f(\mathsf{lim}(x))$ $\displaystyle:\!\!\equiv f_{x,(f,g)[x]}.$ (11.3.2)

Here $(f,g)[x]$ denotes the result of applying $f$ and $g$ to a Cauchy approximation $x$ to obtain a dependent Cauchy approximation over $x$. That is, we define $(f,g)[x]_{\epsilon}:\!\!\equiv f(x_{\epsilon}):A(x_{\epsilon})$, and then for any $\epsilon,\delta:\mathbb{Q}_{+}$ we have $g(x_{\epsilon},x_{\delta},\epsilon+\delta,\xi)$ to witness the fact that $(f,g)[x]$ is a dependent Cauchy approximation, where $\xi:x_{\epsilon}\sim_{\epsilon+\delta}x_{\delta}$ arises from the assumption that $x$ is a Cauchy approximation.

We will never use this notation again, so donβt worry about remembering it. Generally we use the pattern-matching convention, where $f$ is defined by equations such asΒ (11.3.2) andΒ (11.3.2) in which the right-hand side ofΒ (11.3.2) may involve the symbols $f(x_{\epsilon})$ and an assumption that they form a dependent Cauchy approximation.

However, this induction principle is admittedly still quite a mouthful. To help make sense of it, we observe that it contains as special cases two separate induction principles forΒ $\mathbb{R}_{\mathsf{c}}$ and forΒ $\mathord{\sim}$. Firstly, suppose given only a type family $A:\mathbb{R}_{\mathsf{c}}\to\mathcal{U}$, and define $\frown$ to be constant at $\mathbf{1}$. Then much of the required data becomes trivial, and we are left with:

• β’

for any $q:\mathbb{Q}$, an element $f_{q}:A(\mathsf{rat}(q))$,

• β’

for any Cauchy approximation $x$, and any $a:\mathchoice{\prod_{\epsilon:\mathbb{Q}_{+}}\,}{\mathchoice{{\textstyle\prod_% {(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(% \epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\mathchoice{{% \textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})% }}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{% \mathchoice{{\textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:% \mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{% Q}_{+})}}}A(x_{\epsilon})$, an element $f_{x,a}:A(\mathsf{lim}(x))$,

• β’

for $u,v:\mathbb{R}_{\mathsf{c}}$ and $h:\forall(\epsilon:\mathbb{Q}_{+}).\,u\sim_{\epsilon}v$, and $a:A(u)$ and $b:A(v)$, we have $a=^{A}_{\mathsf{eq}_{\mathbb{R}_{\mathsf{c}}}(u,v)}b$.

Given these data, the induction principle yields a function $f:\mathchoice{\prod_{x:\mathbb{R}_{\mathsf{c}}}\,}{\mathchoice{{\textstyle% \prod_{(x:\mathbb{R}_{\mathsf{c}})}}}{\prod_{(x:\mathbb{R}_{\mathsf{c}})}}{% \prod_{(x:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x:\mathbb{R}_{\mathsf{c}})}}}{% \mathchoice{{\textstyle\prod_{(x:\mathbb{R}_{\mathsf{c}})}}}{\prod_{(x:\mathbb% {R}_{\mathsf{c}})}}{\prod_{(x:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x:\mathbb{R}_% {\mathsf{c}})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R}_{\mathsf{c}})}}}{% \prod_{(x:\mathbb{R}_{\mathsf{c}})}}{\prod_{(x:\mathbb{R}_{\mathsf{c}})}}{% \prod_{(x:\mathbb{R}_{\mathsf{c}})}}}A(x)$ such that

 $\displaystyle f(\mathsf{rat}(q))$ $\displaystyle:\!\!\equiv f_{q},$ $\displaystyle f(\mathsf{lim}(x))$ $\displaystyle:\!\!\equiv f_{x,f(x)}.$

We call this principle $\mathbb{R}_{\mathsf{c}}$-induction; it says essentially that if we take $\sim_{\epsilon}$ as given, then $\mathbb{R}_{\mathsf{c}}$ is inductively generated by its constructors.

In particular, if $A$ is a mere property, the third hypothesis in $\mathbb{R}_{\mathsf{c}}$-induction is trivial. Thus, we may prove mere properties of real numbers by simply proving them for rationals and for limits of Cauchy approximations. Here is an example.

###### Lemma 11.3.2.

For any $u:\mathbb{R}_{\mathsf{c}}$ and $\epsilon:\mathbb{Q}_{+}$, we have $u\sim_{\epsilon}u$.

###### Proof.

Define $A(u):\!\!\equiv\forall(\epsilon:\mathbb{Q}_{+}).\,(u\sim_{\epsilon}u)$. Since this is a mere proposition (by the last constructor of $\mathord{\sim}$), by $\mathbb{R}_{\mathsf{c}}$-induction, it suffices to prove it when $u$ is $\mathsf{rat}(q)$ and when $u$ is $\mathsf{lim}(x)$. In the first case, we obviously have $|q-q|<\epsilon$ for any $\epsilon$, hence $\mathsf{rat}(q)\sim_{\epsilon}\mathsf{rat}(q)$ by the first constructor of $\mathord{\sim}$. And in the second case, we may assume inductively that $x_{\delta}\sim_{\epsilon}x_{\delta}$ for all $\delta,\epsilon:\mathbb{Q}_{+}$. Then in particular, we have $x_{\epsilon/3}\sim_{\epsilon/3}x_{\epsilon/3}$, whence $\mathsf{lim}(x)\sim_{\epsilon}\mathsf{lim}(x)$ by the fourth constructor of $\mathord{\sim}$. β

###### Theorem 11.3.3.

$\mathbb{R}_{\mathsf{c}}$ is a set.

###### Proof.

We have just shown that the mere relation $P(u,v):\!\!\equiv\forall(\epsilon:\mathbb{Q}_{+}).\,(u\sim_{\epsilon}v)$ is reflexive. Since it implies identity, by the path constructor of $\mathbb{R}_{\mathsf{c}}$, the result follows from \autorefthm:h-set-refrel-in-paths-sets. β

We can also show that although $\mathbb{R}_{\mathsf{c}}$ may not be a quotient of the set of Cauchy sequences of rationals, it is nevertheless a quotient of the set of Cauchy sequences of reals. (Of course, this is not a valid definition of $\mathbb{R}_{\mathsf{c}}$, but it is a useful property.) We define the type of Cauchy approximations to be

 $\mathcal{C}:\!\!\equiv\setof{x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{c}}|% \forall(\epsilon,\delta:\mathbb{Q}_{+}).\,x_{\delta}\sim_{\delta+\epsilon}x_{% \epsilon}}.$

The second constructor of $\mathbb{R}_{\mathsf{c}}$ gives a function $\mathsf{lim}:\mathcal{C}\to\mathbb{R}_{\mathsf{c}}$.

###### Lemma 11.3.4.

Every real merely is a limit point: $\forall(u:\mathbb{R}_{\mathsf{c}}).\,\exists(x:\mathcal{C}).\,u=\mathsf{lim}(x)$. In other words, $\mathsf{lim}:\mathcal{C}\to\mathbb{R}_{\mathsf{c}}$ is surjective.

###### Proof.

By $\mathbb{R}_{\mathsf{c}}$-induction, we may divide into cases on $u$. Of course, if $u$ is a limit $\mathsf{lim}(x)$, the statement is trivial. So suppose $u$ is a rational point $\mathsf{rat}(q)$; we claim $u$ is equal to $\mathsf{lim}({\lambda}\epsilon.\,\mathsf{rat}(q))$. By the path constructor of $\mathbb{R}_{\mathsf{c}}$, it suffices to show $\mathsf{rat}(q)\sim_{\epsilon}\mathsf{lim}({\lambda}\epsilon.\,\mathsf{rat}(q))$ for all $\epsilon:\mathbb{Q}_{+}$. And by the second constructor of $\mathord{\sim}$, for this it suffices to find $\delta:\mathbb{Q}_{+}$ such that $\mathsf{rat}(q)\sim_{\epsilon-\delta}\mathsf{rat}(q)$. But by the first constructor of $\mathord{\sim}$, we may take any $\delta:\mathbb{Q}_{+}$ with $\delta<\epsilon$. β

###### Lemma 11.3.5.

If $A$ is a set and $f:\mathcal{C}\to A$ respects coincidence of Cauchy approximations, in the sense that

 $\forall(x,y:\mathcal{C}).\,\mathsf{lim}(x)=\mathsf{lim}(y)\Rightarrow f(x)=f(y),$

then $f$ factors uniquely through $\mathsf{lim}:\mathcal{C}\to\mathbb{R}_{\mathsf{c}}$.

###### Proof.

Since $\mathsf{lim}$ is surjective, by \autoreflem:images_are_coequalizers, $\mathbb{R}_{\mathsf{c}}$ is the quotient of $\mathcal{C}$ by the kernel pair of $\mathsf{lim}$. But this is exactly the statement of the lemma. β

For the second special case of the induction principle, suppose instead that we take $A$ to be constant at $\mathbf{1}$. In this case, $\frown$ is simply an $\epsilon$-indexed family of relations on $\epsilon$-close pairs of real numbers, so we may write $u\frown_{\epsilon}v$ instead of $(u,\star)\frown_{\epsilon}(v,\star)$. Then the required data reduces to the following, where $q,r$ denote rational numbers, $\epsilon,\delta,\eta$ positive rational numbers, and $x,y$ Cauchy approximations:

• β’

if $-\epsilon, then $\mathsf{rat}(q)\frown_{\epsilon}\mathsf{rat}(r)$,

• β’

if $\mathsf{rat}(q)\sim_{\epsilon-\delta}y_{\delta}$ and $\mathsf{rat}(q)\frown_{\epsilon-\delta}y_{\delta}$, then $\mathsf{rat}(q)\frown_{\epsilon}\mathsf{lim}(y)$,

• β’

if $x_{\delta}\sim_{\epsilon-\delta}\mathsf{rat}(r)$ and $x_{\delta}\frown_{\epsilon-\delta}\mathsf{rat}(r)$, then $\mathsf{lim}(y)\frown_{\epsilon}\mathsf{rat}(q)$,

• β’

if $x_{\delta}\sim_{\epsilon-\delta-\eta}y_{\eta}$ and $x_{\delta}\frown_{\epsilon-\delta-\eta}y_{\eta}$, then $\mathsf{lim}(x)\frown_{\epsilon}\mathsf{lim}(y)$.

The resulting conclusion is $\forall(u,v:\mathbb{R}_{\mathsf{c}}).\,\forall(\epsilon:\mathbb{Q}_{+}).\,(u% \sim_{\epsilon}v)\to(u\frown_{\epsilon}v)$. We call this principle $\mathord{\sim}$-induction; it says essentially that if we take $\mathbb{R}_{\mathsf{c}}$ as given, then $\sim_{\epsilon}$ is inductively generated (as a family of types) by its constructors. For example, we can use this to show that $\mathord{\sim}$ is symmetric.

###### Lemma 11.3.6.

For any $u,v:\mathbb{R}_{\mathsf{c}}$ and $\epsilon:\mathbb{Q}_{+}$, we have $(u\sim_{\epsilon}v)=(v\sim_{\epsilon}u)$.

###### Proof.

Since both are mere propositions, by symmetry it suffices to show one implication. Thus, let $(u\frown_{\epsilon}v):\!\!\equiv(v\sim_{\epsilon}u)$. By $\mathord{\sim}$-induction, we may reduce to the case that $u\sim_{\epsilon}v$ is derived from one of the four interesting constructors of $\mathord{\sim}$. In the first case when $u$ and $v$ are both rational, the result is trivial (we can apply the first constructor again). In the other three cases, the inductive hypothesis (together with commutativity of addition in $\mathbb{Q}$) yields exactly the input to another of the constructors of $\mathord{\sim}$ (the second and third constructors switch, while the fourth stays put). β

The general induction principle, which we may call $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-induction, is therefore a sort of joint $\mathbb{R}_{\mathsf{c}}$-induction and $\mathord{\sim}$-induction. Consider, for instance, its non-dependent version, which we call $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion, which is the one that we will have the most use for. Ordinary $\mathbb{R}_{\mathsf{c}}$-recursion tells us that to define a function $f:\mathbb{R}_{\mathsf{c}}\to A$ it suffices to:

1. 1.

for every $q:\mathbb{Q}$ construct $f(\mathsf{rat}(q)):A$,

2. 2.

for every Cauchy approximation $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{c}}$, construct $f(x):A$, assuming that $f(x_{\epsilon})$ has already been defined for all $\epsilon:\mathbb{Q}_{+}$,

3. 3.

prove $f(u)=f(v)$ for all $u,v:\mathbb{R}_{\mathsf{c}}$ satisfying $\forall(\epsilon:\mathbb{Q}_{+}).\,u\sim_{\epsilon}v$.

However, it is generally quite difficult to showΒ 3 without knowing something about how $f$ acts on $\epsilon$-close Cauchy reals. The enhanced principle of $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion remedies this deficiency, allowing us to specify an arbitrary βway in which $f$ acts on $\epsilon$-close Cauchy realsβ, which we can then prove to be the case by a simultaneous induction with the definition of $f$. This is the family of relations $\frown$. Since $A$ is independent of $\mathbb{R}_{\mathsf{c}}$, we may assume for simplicity that $\frown$ depends only on $A$ and $\mathbb{Q}_{+}$, and thus there is no ambiguity in writing $a\frown_{\epsilon}b$ instead of $(u,a)\frown_{\epsilon}(v,b)$. In this case, defining a function $f:\mathbb{R}_{\mathsf{c}}\to A$ by $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion requires the following cases (which we now write using the pattern-matching convention).

• β’

For every $q:\mathbb{Q}$, construct $f(\mathsf{rat}(q)):A$.

• β’

For every Cauchy approximation $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{c}}$, construct $f(x):A$, assuming inductively that $f(x_{\epsilon})$ has already been defined for all $\epsilon:\mathbb{Q}_{+}$ and form a βCauchy approximation with respect to $\frown$β, i.e.Β that $\forall(\epsilon,\delta:\mathbb{Q}_{+}).\,(f(x_{\epsilon})\frown_{\epsilon+% \delta}f(x_{\delta}))$.

• β’

Prove that the relations $\frown$ are separated, i.e.Β that, for any $a,b:A$, $(\forall(\epsilon:\mathbb{Q}_{+}).\,a\frown_{\epsilon}b)\Rightarrow(a=b).$

• β’

Prove that if $-\epsilon for $q,r:\mathbb{Q}$, then $f(\mathsf{rat}(q))\frown_{\epsilon}f(\mathsf{rat}(r))$.

• β’

For any $q:\mathbb{Q}$ and any Cauchy approximation $y$, prove that $f(\mathsf{rat}(q))\frown_{\epsilon}f(\mathsf{lim}(y)),$ assuming inductively that $\mathsf{rat}(q)\sim_{\epsilon-\delta}y_{\delta}$ and $f(\mathsf{rat}(q))\frown_{\epsilon-\delta}f(y_{\delta})$ for some $\delta:\mathbb{Q}_{+}$, and that $\eta\mapsto f(x_{\eta})$ is a Cauchy approximation with respect to $\frown$.

• β’

For any Cauchy approximation $x$ and any $r:\mathbb{Q}$, prove that $f(\mathsf{lim}(x))\frown_{\epsilon}f(\mathsf{rat}(r)),$ assuming inductively that $x_{\delta}\sim_{\epsilon-\delta}\mathsf{rat}(r)$ and $f(x_{\delta})\frown_{\epsilon-\delta}f(\mathsf{rat}(r))$ for some $\delta:\mathbb{Q}_{+}$, and that $\eta\mapsto f(x_{\eta})$ is a Cauchy approximation with respect to $\frown$.

• β’

For any Cauchy approximations $x,y$, prove that $f(\mathsf{lim}(x))\frown_{\epsilon}f(\mathsf{lim}(y)),$ assuming inductively that $x_{\delta}\sim_{\epsilon-\delta-\eta}y_{\eta}$ and $f(x_{\delta})\frown_{\epsilon-\delta-\eta}f(y_{\eta})$ for some $\delta,\eta:\mathbb{Q}_{+}$, and that $\theta\mapsto f(x_{\theta})$ and $\theta\mapsto f(y_{\theta})$ are Cauchy approximations with respect to $\frown$.

Note that in the last four proofs, we are free to use the specific definitions of $f(\mathsf{rat}(q))$ and $f(\mathsf{lim}(x))$ given in the first two data. However, the proof of separatedness must apply to any two elements of $A$, without any relation to $f$: it is a sort of βadmissibilityβ condition on the family of relations $\frown$. Thus, we often verify it first, immediately after defining $\frown$, before going on to define $f(\mathsf{rat}(q))$ and $f(\mathsf{lim}(x))$.

Under the above hypotheses, $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion yields a function $f:\mathbb{R}_{\mathsf{c}}\to A$ such that $f(\mathsf{rat}(q))$ and $f(\mathsf{lim}(x))$ are judgmentally equal to the definitions given for them in the first two clauses. Moreover, we may also conclude

 $\forall(u,v:\mathbb{R}_{\mathsf{c}}).\,\forall(\epsilon:\mathbb{Q}_{+}).\,(u% \sim_{\epsilon}v)\to(f(u)\frown_{\epsilon}f(v)).$ (11.3.7)

As a paradigmatic example, $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion allows us to extend functions defined on $\mathbb{Q}$ to all of $\mathbb{R}_{\mathsf{c}}$, as long as they are sufficiently continuous.

###### Definition 11.3.8.

A function $f:\mathbb{Q}\to\mathbb{R}_{\mathsf{c}}$ is if there exists $L:\mathbb{Q}_{+}$ (the Lipschitz constant) such that

 $|q-r|<\epsilon\Rightarrow(f(q)\sim_{L\epsilon}f(r))$

for all $\epsilon:\mathbb{Q}_{+}$ and $q,r:\mathbb{Q}$. Similarly, $g:\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}$ is Lipschitz if there exists $L:\mathbb{Q}_{+}$ such that

 $(u\sim_{\epsilon}v)\Rightarrow(g(u)\sim_{L\epsilon}g(v))$

for all $\epsilon:\mathbb{Q}_{+}$ and $u,v:\mathbb{R}_{\mathsf{c}}$..

In particular, note that by the first constructor of $\mathord{\sim}$, if $f:\mathbb{Q}\to\mathbb{Q}$ is Lipschitz in the obvious sense, then so is the composite $\mathbb{Q}\xrightarrow{f}\mathbb{Q}\to\mathbb{R}_{\mathsf{c}}$.

###### Lemma 11.3.9.

Suppose $f:\mathbb{Q}\to\mathbb{R}_{\mathsf{c}}$ is Lipschitz with constant $L:\mathbb{Q}_{+}$. Then there exists a Lipschitz map $\bar{f}:\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}$, also with constant $L$, such that $\bar{f}(\mathsf{rat}(q))\equiv f(q)$ for all $q:\mathbb{Q}$.

###### Proof.

We define $\bar{f}$ by $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion, with codomain $A:\!\!\equiv\mathbb{R}_{\mathsf{c}}$. We define the relation $\mathord{\frown}:\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}\to\mathbb{Q% }_{+}\to\mathsf{Prop}$ to be

 $\displaystyle(u\frown_{\epsilon}v)$ $\displaystyle:\!\!\equiv(u\sim_{L\epsilon}v).$

For $q:\mathbb{Q}$, we define

 $\bar{f}(\mathsf{rat}(q)):\!\!\equiv\mathsf{rat}(f(q)).$

For a Cauchy approximation $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{c}}$, we define

 $\bar{f}(\mathsf{lim}(x)):\!\!\equiv\mathsf{lim}({\lambda}\epsilon.\,\bar{f}(x_% {\epsilon/L})).$

For this to make sense, we must verify that $y:\!\!\equiv{\lambda}\epsilon.\,\bar{f}(x_{\epsilon/L})$ is a Cauchy approximation. However, the inductive hypothesis for this step is that for any $\delta,\epsilon:\mathbb{Q}_{+}$ we have $\bar{f}(x_{\delta})\frown_{\delta+\epsilon}\bar{f}(x_{\epsilon})$, i.e.Β $\bar{f}(x_{\delta})\sim_{L\delta+L\epsilon}\bar{f}(x_{\epsilon})$. Thus we have

 $y_{\delta}\equiv f(x_{\delta/L})\sim_{\delta+\epsilon}f(x_{\epsilon/L})\equiv y% _{\epsilon}.$

For proving separatedness, we simply observe that $\forall(\epsilon:\mathbb{Q}_{+}).\,a\frown_{\epsilon}b$ means $\forall(\epsilon:\mathbb{Q}_{+}).\,a\sim_{L\epsilon}b$, which implies $\forall(\epsilon:\mathbb{Q}_{+}).\,a\sim_{\epsilon}b$ and thus $a=b$.

To complete the $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion, it remains to verify the four conditions on $\frown$. This basically amounts to proving that $\bar{f}$ is Lipschitz for all the four constructors of $\mathord{\sim}$.

1. 1.

When $u$ is $\mathsf{rat}(q)$ and $v$ is $\mathsf{rat}(r)$ with $-\epsilon<|q-r|<\epsilon$, the assumption that $f$ is Lipschitz yields $f(q)\sim_{L\epsilon}f(r)$, hence $\bar{f}(\mathsf{rat}(q))\frown_{\epsilon}\bar{f}(\mathsf{rat}(r))$ by definition.

2. 2.

When $u$ is $\mathsf{lim}(x)$ and $v$ is $\mathsf{rat}(q)$ with $x_{\eta}\sim_{\epsilon-\eta}\mathsf{rat}(q)$, then the inductive hypothesis is $\bar{f}(x_{\eta})\sim_{L\epsilon-L\eta}\mathsf{rat}(f(q))$, which proves $\bar{f}(\mathsf{lim}(x))\sim_{L\epsilon}\bar{f}(\mathsf{rat}(q))$ by the third constructor of $\mathord{\sim}$.

3. 3.

The symmetric case when $u$ is rational and $v$ is a limit is essentially identical.

4. 4.

When $u$ is $\mathsf{lim}(x)$ and $v$ is $\mathsf{lim}(y)$, with $\delta,\eta:\mathbb{Q}_{+}$ such that $x_{\delta}\sim_{\epsilon-\delta-\eta}y_{\eta}$, the inductive hypothesis is $\bar{f}(x_{\delta})\sim_{L\epsilon-L\delta-L\eta}\bar{f}(y_{\eta})$, which proves $\bar{f}(\mathsf{lim}(x))\sim_{L\epsilon}\bar{f}(\mathsf{lim}(y))$ by the fourth constructor of $\mathord{\sim}$.

This completes the $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion, and hence the construction of $\bar{f}$. The desired equality $\bar{f}(\mathsf{rat}(q))\equiv f(q)$ is exactly the first computation rule for $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion, and the additional conditionΒ (11.3.7) says exactly that $\bar{f}$ is Lipschitz with constant $L$. β

At this point we have gone about as far as we can without a better characterization of $\mathord{\sim}$. We have specified, in the constructors of $\mathord{\sim}$, the conditions under which we want Cauchy reals of the two different forms to be $\epsilon$-close. However, how do we know that in the resulting inductive-inductive type family, these are the only witnesses to this fact? We have seen that inductive type families (such as identity types, see \autorefsec:identity-systems) and higher inductive types have a tendency to contain βmore than was put into themβ, so this is not an idle question.

In order to characterize $\mathord{\sim}$ more precisely, we will define a family of relations $\approx_{\epsilon}$ on $\mathbb{R}_{\mathsf{c}}$ recursively, so that they will compute on constructors, and prove that this family is equivalent to $\sim_{\epsilon}$.

###### Theorem 11.3.10.

There is a family of mere relations $\mathord{\approx}:\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}\to\mathbb{% Q}_{+}\to\mathsf{Prop}$ such that

 $\displaystyle(\mathsf{rat}(q)\approx_{\epsilon}\mathsf{rat}(r))$ $\displaystyle:\!\!\equiv(-\epsilon (11.3.10) $\displaystyle(\mathsf{rat}(q)\approx_{\epsilon}\mathsf{lim}(y))$ $\displaystyle:\!\!\equiv\exists(\delta:\mathbb{Q}_{+}).\,\mathsf{rat}(q)% \approx_{\epsilon-\delta}y_{\delta}$ (11.3.10) $\displaystyle(\mathsf{lim}(x)\approx_{\epsilon}\mathsf{rat}(r))$ $\displaystyle:\!\!\equiv\exists(\delta:\mathbb{Q}_{+}).\,x_{\delta}\approx_{% \epsilon-\delta}\mathsf{rat}(r)$ (11.3.10) $\displaystyle(\mathsf{lim}(x)\approx_{\epsilon}\mathsf{lim}(y))$ $\displaystyle:\!\!\equiv\exists(\delta,\eta:\mathbb{Q}_{+}).\,x_{\delta}% \approx_{\epsilon-\delta-\eta}y_{\eta}.$ (11.3.10)

Moreover, we have

 $\displaystyle(u\approx_{\epsilon}v)\Leftrightarrow\exists(\theta:\mathbb{Q}_{+% }).\,(u\approx_{\epsilon-\theta}v)$ (11.3.10) $\displaystyle(u\approx_{\epsilon}v)\to(v\sim_{\delta}w)\to(u\approx_{\epsilon+% \delta}w)$ (11.3.10) $\displaystyle(u\sim_{\epsilon}v)\to(v\approx_{\delta}w)\to(u\approx_{\epsilon+% \delta}w).$ (11.3.10)

The additional conditionsΒ (11.3.10)β(11.3.10) turn out to be required in order to make the inductive definition go through. ConditionΒ (11.3.10) is called being rounded. Reading it from right to left gives monotonicity of $\approx$,

 $(\delta<\epsilon)\land(u\approx_{\delta}v)\Rightarrow(u\approx_{\epsilon}v)$

while reading it left to right to openness of $\approx$,

 $(u\approx_{\epsilon}v)\Rightarrow\exists(\epsilon:\mathbb{Q}_{+}).\,(\delta<% \epsilon)\land(u\approx_{\delta}v).$

ConditionsΒ (11.3.10) andΒ (11.3.10) are forms of the triangle inequality, which say that $\approx$ is a βmoduleβ over $\mathord{\sim}$ on both sides.

###### Proof.

We will define $\mathord{\approx}:\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}\to\mathbb{% Q}_{+}\to\mathsf{Prop}$ by double $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion. First we will apply $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion with codomain the subset of $\mathbb{R}_{\mathsf{c}}\to\mathbb{Q}_{+}\to\mathsf{Prop}$ consisting of those families of predicates which are rounded and satisfy the one appropriate form of the triangle inequality. Thinking of these predicates as half of a binary relation, we will write them as $(u,\epsilon)\mapsto(\diamondsuit\approx_{\epsilon}u)$, with the symbol $\diamondsuit$ referring to the whole relation. Now we can write $A$ precisely as

 $\displaystyle A:\!\!\equiv\;\Bigg{\{}\diamondsuit:\mathbb{R}_{\mathsf{c}}\to% \mathbb{Q}_{+}\to\mathsf{Prop}\;\bigg{|}\\ \displaystyle\Big{(}\forall(u:\mathbb{R}_{\mathsf{c}}).\,\forall(\epsilon:% \mathbb{Q}_{+}).\,\big{(}(\diamondsuit\approx_{\epsilon}u)\Leftrightarrow% \exists(\theta:\mathbb{Q}_{+}).\,(\diamondsuit\approx_{\epsilon-\theta}u)\big{% )}\Big{)}\\ \displaystyle\land\Big{(}\forall(u,v:\mathbb{R}_{\mathsf{c}}).\,\forall(\eta,% \epsilon:\mathbb{Q}_{+}).\,(u\sim_{\epsilon}v)\to\\ \displaystyle\big{(}(\diamondsuit\approx_{\eta}u)\to(\diamondsuit\approx_{\eta% +\epsilon}v)\big{)}\land\big{(}(\diamondsuit\approx_{\eta}v)\to(\diamondsuit% \approx_{\eta+\epsilon}u)\big{)}\Big{)}\Bigg{\}}$

As usual with subsets, we will use the same notation for an inhabitant of $A$ and its first component $\diamondsuit$. As the family of relations required for $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion, we consider the following, which will ensure the other form of the triangle inequality:

 $(\diamondsuit\frown_{\epsilon}\heartsuit):\!\!\equiv\forall(u:\mathbb{R}_{% \mathsf{c}}).\,\forall(\eta:\mathbb{Q}_{+}).\,((\diamondsuit\approx_{\eta}u)% \to(\heartsuit\approx_{\epsilon+\eta}u))\land((\heartsuit\approx_{\eta}u)\to(% \diamondsuit\approx_{\epsilon+\eta}u)).$

We observe that these relations are separated. For assuming $\forall(\epsilon:\mathbb{Q}_{+}).\,(\diamondsuit\frown_{\epsilon}\heartsuit),$ to show $\diamondsuit=\heartsuit$ it suffices to show $(\diamondsuit\approx_{\epsilon}u)\Leftrightarrow(\heartsuit\approx_{\epsilon}u)$ for all $u:\mathbb{R}_{\mathsf{c}}$. But $\diamondsuit\approx_{\epsilon}u$ implies $\diamondsuit\approx_{\epsilon-\theta}u$ for some $\theta$, by roundedness, which together with $\diamondsuit\frown_{\epsilon}\heartsuit$ implies $\heartsuit\approx_{\epsilon}u$; and the converse is identical.

Now the first two data the recursion principle requires are the following.

• β’

For any $q:\mathbb{Q}$, we must give an element of $A$, which we denote $(\mathsf{rat}(q)\approx_{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}% \mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$.

• β’

For any Cauchy approximation $x$, if we assume defined a function $\mathbb{Q}_{+}\to A$, which we will denote by $\epsilon\mapsto(x_{\epsilon}\approx_{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0% pt})}\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$, with the property that

 $\forall(u:\mathbb{R}_{\mathsf{c}}).\,\forall(\delta,\epsilon,\eta:\mathbb{Q}_{% +}).\,(x_{\delta}\approx_{\eta}u)\to(x_{\epsilon}\approx_{\eta+\delta+\epsilon% }u),$ (11.3.11)

we must give an element of $A$, which we write as $(\mathsf{lim}(x)\approx_{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}% \mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$.

In both cases, we give the required definition by using a nested $(\mathbb{R}_{\mathsf{c}},\mathord{\sim})$-recursion, with codomain the subset of $\mathbb{Q}_{+}\to\mathsf{Prop}$ consisting of rounded families of mere propositions. Thinking of these propositions as zero halves of a binary relation, we will write them as $\epsilon\mapsto(\bullet\approx_{\epsilon}\triangle)$, with the symbol $\triangle$ referring to the whole family. Now we can write the codomain of these inner recursions precisely as

 $C:\!\!\equiv\bigg{\{}\triangle:\mathbb{Q}_{+}\to\mathsf{Prop}\;\;\Big{|}\;\;% \forall(\epsilon:\mathbb{Q}_{+}).\,\Big{(}(\bullet\approx_{\epsilon}\triangle)% \Leftrightarrow\exists(\theta:\mathbb{Q}_{+}).\,(\bullet\approx_{\epsilon-% \theta}\triangle)\Big{)}\bigg{\}}$

We take the required family of relations to be the remnant of the triangle inequality:

 $(\triangle\smile_{\epsilon}\square):\!\!\equiv\forall(\eta:\mathbb{Q}_{+}).\,(% (\bullet\approx_{\eta}\triangle)\to(\bullet\approx_{\epsilon+\eta}\square))% \land((\bullet\approx_{\eta}\square)\to(\bullet\approx_{\epsilon+\eta}% \triangle)).$

These relations are separated by the same argument as for $\frown$, using roundedness of all elements of $C$.

Note that if such an inner recursion succeeds, it will yield a family of predicates $\diamondsuit:\mathbb{R}_{\mathsf{c}}\to\mathbb{Q}_{+}\to\mathsf{Prop}$ which are rounded (since their image in $\mathbb{Q}_{+}\to\mathsf{Prop}$ lies in $C$) and satisfy

 $\forall(u,v:\mathbb{R}_{\mathsf{c}}).\,\forall(\epsilon:\mathbb{Q}_{+}).\,(u% \sim_{\epsilon}v)\to\big{(}(\diamondsuit\approx_{(\mathord{\hskip 1.0pt\text{-% -}\hskip 1.0pt})}u)\smile_{\epsilon}(\diamondsuit\approx_{(\mathord{\hskip 1.0% pt\text{--}\hskip 1.0pt})}u)\big{)}.$

Expanding out the definition of $\smile$, this yields precisely the third condition for $\diamondsuit$ to belong to $A$; thus it is exactly what we need.

It is at this point that we can give the definitionsΒ (11.3.10)β(11.3.10), as the first two clauses of each of the two inner recursions, corresponding to rational points and limits. In each case, we must verify that the relation is rounded and hence lies in $C$. In the rational-rational caseΒ (11.3.10) this is clear, while in the other cases it follows from an inductive hypothesis. (InΒ (11.3.10) the relevant inductive hypothesis is that $(\mathsf{rat}(q)\approx_{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}y_{% \delta}):C$, while inΒ (11.3.10) andΒ (11.3.10) it is that $(x_{\delta}\approx_{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt}):A$.)

The remaining data of the sub-recursions consist of showing that (11.3.10)β(11.3.10) satisfy the triangle inequality on the right with respect to the constructors of $\mathord{\sim}$. There are eight cases β four in each sub-recursion β corresponding to the eight possible ways that $u$, $v$, and $w$ inΒ (11.3.10) can be chosen to be rational points or limits. First we consider the cases when $u$ is $\mathsf{rat}(q)$.

1. 1.

Assuming $\mathsf{rat}(q)\approx_{\phi}\mathsf{rat}(r)$ and $-\epsilon<|r-s|<\epsilon$, we must show $\mathsf{rat}(q)\approx_{\phi+\epsilon}\mathsf{rat}(s)$. But by definition of $\approx$, this reduces to the triangle inequality for rational numbers.

2. 2.

We assume $\phi,\epsilon,\delta:\mathbb{Q}_{+}$ such that $\mathsf{rat}(q)\approx_{\phi}\mathsf{rat}(r)$ and $\mathsf{rat}(r)\sim_{\epsilon-\delta}y_{\delta}$, and inductively that

 $\forall(\psi:\mathbb{Q}_{+}).\,(\mathsf{rat}(q)\approx_{\psi}\mathsf{rat}(r))% \to(\mathsf{rat}(q)\approx_{\psi+\epsilon-\delta}y_{\delta}).$ (11.3.12)

We assume also that $\psi,\delta\mapsto(\mathsf{rat}(q)\approx_{\psi}y_{\delta})$ is a Cauchy approximation with respect to $\smile$, i.e.

 $\forall(\psi,\xi,\zeta:\mathbb{Q}_{+}).\,(\mathsf{rat}(q)\approx_{\psi}y_{\xi}% )\to(\mathsf{rat}(q)\approx_{\psi+\xi+\zeta}y_{\zeta}),$ (11.3.13)

although we do not need this assumption in this case. Indeed, (11.3.12) with $\psi:\!\!\equiv\phi$ yields immediately $\mathsf{rat}(q)\approx_{\phi+\epsilon-\delta}y_{\delta}$, and hence $\mathsf{rat}(q)\approx_{\phi+\epsilon}\mathsf{lim}(y)$ by definition of $\approx$.

3. 3.

We assume $\phi,\epsilon,\delta:\mathbb{Q}_{+}$ such that $\mathsf{rat}(q)\approx_{\phi}\mathsf{lim}(y)$ and $y_{\delta}\sim_{\epsilon-\delta}\mathsf{rat}(r)$, and inductively that

 $\displaystyle\forall(\psi:\mathbb{Q}_{+}).\,(\mathsf{rat}(q)\approx_{\psi}y_{% \delta})\to(\mathsf{rat}(q)\approx_{\psi+\epsilon-\delta}\mathsf{rat}(r)).$ (11.3.14) $\displaystyle\forall(\psi,\xi,\zeta:\mathbb{Q}_{+}).\,(\mathsf{rat}(q)\approx_% {\psi}y_{\xi})\to(\mathsf{rat}(q)\approx_{\psi+\xi+\zeta}y_{\zeta}).$ (11.3.14)

By definition, $\mathsf{rat}(q)\approx_{\phi}\mathsf{lim}(y)$ means that we have $\theta:\mathbb{Q}_{+}$ with $\mathsf{rat}(q)\approx_{\phi-\theta}y_{\theta}$. By assumptionΒ (11.3.14), therefore, we have also $\mathsf{rat}(q)\approx_{\phi+\delta}y_{\delta}$, and then byΒ (11.3.14) it follows that $\mathsf{rat}(q)\approx_{\phi+\epsilon}\mathsf{rat}(r)$, as desired.

4. 4.

We assume $\phi,\epsilon,\delta,\eta:\mathbb{Q}_{+}$ such that $\mathsf{rat}(q)\approx_{\phi}\mathsf{lim}(y)$ and $y_{\delta}\sim_{\epsilon-\delta-\eta}z_{\eta}$, and inductively that

 $\displaystyle\forall(\psi:\mathbb{Q}_{+}).\,(\mathsf{rat}(q)\approx_{\psi}y_{% \delta})\to(\mathsf{rat}(q)\approx_{\psi+\epsilon-\delta-\eta}z_{\eta}),$ (11.3.14) $\displaystyle\forall(\psi,\xi,\zeta:\mathbb{Q}_{+}).\,(\mathsf{rat}(q)\approx_% {\psi}y_{\xi})\to(\mathsf{rat}(q)\approx_{\psi+\xi+\zeta}y_{\zeta}),$ (11.3.14) $\displaystyle\forall(\psi,\xi,\zeta:\mathbb{Q}_{+}).\,(\mathsf{rat}(q)\approx_% {\psi}z_{\xi})\to(\mathsf{rat}(q)\approx_{\psi+\xi+\zeta}z_{\zeta}).$ (11.3.14)

Again, $\mathsf{rat}(q)\approx_{\phi}\mathsf{lim}(y)$ means we have $\xi:\mathbb{Q}_{+}$ with $\mathsf{rat}(q)\approx_{\phi-\xi}y_{\xi}$, whileΒ (11.3.14) then implies $\mathsf{rat}(q)\approx_{\phi+\delta}y_{\delta}$ andΒ (11.3.14) implies $\mathsf{rat}(q)\approx_{\phi+\epsilon-\eta}z_{\eta}$. But by definition of $\approx$, this implies $\mathsf{rat}(q)\approx_{\phi+\epsilon}\mathsf{lim}(z)$ as desired.

Now we move on to the cases when $u$ is $\mathsf{lim}(x)$, with $x$ a Cauchy approximation. In this case, the ambient inductive hypothesis of the definition of $(\mathsf{lim}(x)\approx_{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}{% \mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}}):A$ is that we have ${(x_{\delta}\approx_{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}{\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt}})}:A$, so that in addition to being rounded they satisfy the triangle inequality on the right.

1. 5.

Assuming $\mathsf{lim}(x)\approx_{\phi}\mathsf{rat}(r)$ and $-\epsilon<|r-s|<\epsilon$, we must show $\mathsf{lim}(x)\approx_{\phi+\epsilon}\mathsf{rat}(s)$. By definition of $\approx$, the former means $x_{\delta}\approx_{\phi-\delta}\mathsf{rat}(r)$, so that above triangle inequality implies $x_{\delta}\approx_{\epsilon+\phi-\delta}\mathsf{rat}(s)$, hence $\mathsf{lim}(x)\approx_{\phi+\epsilon}\mathsf{rat}(s)$ as desired.

2. 6.

We assume $\phi,\epsilon,\delta:\mathbb{Q}_{+}$ such that $\mathsf{lim}(x)\approx_{\phi}\mathsf{rat}(r)$ and $\mathsf{rat}(r)\sim_{\epsilon-\delta}y_{\delta}$, and two unneeded inductive hypotheses. By definition, we have $\eta:\mathbb{Q}_{+}$ such that $x_{\eta}\approx_{\phi-\eta}\mathsf{rat}(r)$, so the inductive triangle inequality gives $x_{\eta}\approx_{\phi+\epsilon-\eta-\delta}y_{\delta}$. The definition of $\approx$ then immediately yields $\mathsf{lim}(x)\approx_{\phi+\epsilon}\mathsf{lim}(y)$.

3. 7.

We assume $\phi,\epsilon,\delta:\mathbb{Q}_{+}$ such that $\mathsf{lim}(x)\approx_{\phi}\mathsf{lim}(y)$ and $y_{\delta}\sim_{\epsilon-\delta}\mathsf{rat}(r)$, and two unneeded inductive hypotheses. By definition we have $\xi,\theta:\mathbb{Q}_{+}$ such that $x_{\xi}\approx_{\phi-\xi-\theta}y_{\theta}$. Since $y$ is a Cauchy approximation, we have $y_{\theta}\sim_{\theta+\delta}y_{\delta}$, so the inductive triangle inequality gives $x_{\xi}\approx_{\phi+\delta-\xi}y_{\delta}$ and then $x_{\xi}\sim_{\phi+\epsilon-\xi}\mathsf{rat}(r)$. The definition of $\approx$ then gives $\mathsf{lim}(x)\approx_{\phi+\epsilon}\mathsf{rat}(r)$, as desired.

4. 8.

Finally, we assume $\phi,\epsilon,\delta,\eta:\mathbb{Q}_{+}$ such that $\mathsf{lim}(x)\approx_{\phi}\mathsf{lim}(y)$ and $y_{\delta}\sim_{\epsilon-\delta-\eta}z_{\eta}$. Then as before we have $\xi,\theta:\mathbb{Q}_{+}$ with $x_{\xi}\approx_{\phi-\xi-\theta}y_{\theta}$, and two applications of the triangle inequality suffices as before.

This completes the two inner recursions, and thus the definitions of the families of relations $(\mathsf{rat}(q)\approx_{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}% \mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ and $(\mathsf{lim}(x)\approx_{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}% \mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$. Since all are elements of $A$, they are rounded and satisfy the triangle inequality on the right with respect to $\mathord{\sim}$. What remains is to verify the conditions relating to $\frown$, which is to say that these relations satisfy the triangle inequality on the left with respect to the constructors of $\mathord{\sim}$. The four cases correspond to the four choices of rational or limit points for $u$ and $v$ inΒ (11.3.10), and since they are all mere propositions, we may apply $\mathbb{R}_{\mathsf{c}}$-induction and assume that $w$ is also either rational or a limit. This yields another eight cases, whose proofs are essentially identical to those just given; so we will not subject the reader to them. β

We can now prove:

###### Theorem 11.3.14.

For any $u,v:\mathbb{R}_{\mathsf{c}}$ and $\epsilon:\mathbb{Q}_{+}$ we have $(u\sim_{\epsilon}v)=(u\approx_{\epsilon}v)$.

###### Proof.

Since both are mere propositions, it suffices to prove bidirectional implication. For the left-to-right direction, we use $\mathord{\sim}$-induction applied to $C(u,v,\epsilon):\!\!\equiv(u\approx_{\epsilon}v)$. Thus, it suffices to consider the four constructors of $\mathord{\sim}$. In each case, $u$ and $v$ are specialized to either rational points or limits, so that the definition of $\approx$ evaluates, and the inductive hypothesis always applies.

For the right-to-left direction, we use $\mathbb{R}_{\mathsf{c}}$-induction to assume that $u$ and $v$ are rational points or limits, allowing $\approx$ to evaluate. But now the definitions of $\approx$, and the inductive hypotheses, supply exactly the data required for the relevant constructors of $\mathord{\sim}$. β

Stretching a point, one might call $\approx$ a fibration of βcodesβ for $\mathord{\sim}$, with the two directions of the above proof being $\mathsf{encode}$ and $\mathsf{decode}$ respectively. By the definition of $\approx$, from \autorefthm:RC-sim-characterization we get equivalences

 $\displaystyle(\mathsf{rat}(q)\sim_{\epsilon}\mathsf{rat}(r))$ $\displaystyle=(-\epsilon $\displaystyle(\mathsf{rat}(q)\sim_{\epsilon}\mathsf{lim}(y))$ $\displaystyle=\exists(\delta:\mathbb{Q}_{+}).\,\mathsf{rat}(q)\sim_{\epsilon-% \delta}y_{\delta}$ $\displaystyle(\mathsf{lim}(x)\sim_{\epsilon}\mathsf{rat}(r))$ $\displaystyle=\exists(\delta:\mathbb{Q}_{+}).\,x_{\delta}\sim_{\epsilon-\delta% }\mathsf{rat}(r)$ $\displaystyle(\mathsf{lim}(x)\sim_{\epsilon}\mathsf{lim}(y))$ $\displaystyle=\exists(\delta,\eta:\mathbb{Q}_{+}).\,x_{\delta}\sim_{\epsilon-% \delta-\eta}y_{\eta}.$

Our proof also provides the following additional information.

###### Corollary 11.3.15.

$\mathord{\sim}$ is rounded and satisfies the triangle inequality:

 $\displaystyle(u\sim_{\epsilon}v)\;\simeq\;\exists(\theta:\mathbb{Q}_{+}).\,u% \sim_{\epsilon-\theta}v$ (11.3.15) $\displaystyle(u\sim_{\epsilon}v)\to(v\sim_{\delta}w)\to(u\sim_{\epsilon+\delta% }w).$ (11.3.15)

With the triangle inequality in hand, we can show that βlimitsβ of Cauchy approximations actually behave like limits.

###### Lemma 11.3.16.

For any $u:\mathbb{R}_{\mathsf{c}}$, Cauchy approximation $y$, and $\epsilon,\delta:\mathbb{Q}_{+}$, if $u\sim_{\epsilon}y_{\delta}$ then $u\sim_{\epsilon+\delta}\mathsf{lim}(y)$.

###### Proof.

We use $\mathbb{R}_{\mathsf{c}}$-induction on $u$. If $u$ is $\mathsf{rat}(q)$, then this is exactly the second constructor of $\mathord{\sim}$. Now suppose $u$ is $\mathsf{lim}(x)$, and that each $x_{\eta}$ has the property that for any $y,\epsilon,\delta$, if $x_{\eta}\sim_{\epsilon}y_{\delta}$ then $x_{\eta}\sim_{\epsilon+\delta}\mathsf{lim}(y)$. In particular, taking $y:\!\!\equiv x$ and $\delta:\!\!\equiv\eta$ in this assumption, we conclude that $x_{\eta}\sim_{\eta+\theta}\mathsf{lim}(x)$ for any $\eta,\theta:\mathbb{Q}_{+}$.

Now let $y,\epsilon,\delta$ be arbitrary and assume $\mathsf{lim}(x)\sim_{\epsilon}y_{\delta}$. By roundedness, there is a $\theta$ such that $\mathsf{lim}(x)\sim_{\epsilon-\theta}y_{\delta}$. Then by the above observation, for any $\eta$ we have $x_{\eta}\sim_{\eta+\theta/2}\mathsf{lim}(x)$, and hence $x_{\eta}\sim_{\epsilon+\eta-\theta/2}y_{\delta}$ by the triangle inequality. Hence, the fourth constructor of $\mathord{\sim}$ yields $\mathsf{lim}(x)\sim_{\epsilon+2\eta+\delta-\theta/2}\mathsf{lim}(y)$. Thus, if we choose $\eta:\!\!\equiv\theta/4$, the result follows. β

###### Lemma 11.3.17.

For any Cauchy approximation $y$ and any $\delta,\eta:\mathbb{Q}_{+}$ we have $y_{\delta}\sim_{\delta+\eta}\mathsf{lim}(y)$.

###### Proof.

Take $u:\!\!\equiv y_{\delta}$ and $\epsilon:\!\!\equiv\eta$ in the previous lemma. β

###### Remark 11.3.18.

We might have expected to have $y_{\delta}\sim_{\delta}\mathsf{lim}(y)$, but this fails in examples. For instance, consider $x$ defined by $x_{\epsilon}:\!\!\equiv\epsilon$. Its limit is clearly $0$, but we do not have $|\epsilon-0|<\epsilon$, only $\leq$.

As an application, \autorefthm:RC-sim-lim-term enables us to show that the extensions of Lipschitz functions from \autorefRC-extend-Q-Lipschitz are unique.

###### Lemma 11.3.19.

Let $f,g:\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}$ be continuous, in the sense that

 $\forall(u:\mathbb{R}_{\mathsf{c}}).\,\forall(\epsilon:\mathbb{Q}_{+}).\,% \exists(\delta:\mathbb{Q}_{+}).\,\forall(v:\mathbb{R}_{\mathsf{c}}).\,(u\sim_{% \delta}v)\to(f(u)\sim_{\epsilon}f(v))$

and analogously for $g$. If $f(\mathsf{rat}(q))=g(\mathsf{rat}(q))$ for all $q:\mathbb{Q}$, then $f=g$.

###### Proof.

We prove $f(u)=g(u)$ for all $u$ by $\mathbb{R}_{\mathsf{c}}$-induction. The rational case is just the hypothesis. Thus, suppose $f(x_{\delta})=g(x_{\delta})$ for all $\delta$. We will show that $f(\mathsf{lim}(x))\sim_{\epsilon}g(\mathsf{lim}(x))$ for all $\epsilon$, so that the path constructor of $\mathbb{R}_{\mathsf{c}}$ applies.

Since $f$ and $g$ are continuous, there exist $\theta,\eta$ such that for all $v$, we have

 $\displaystyle(\mathsf{lim}(x)\sim_{\theta}v)$ $\displaystyle\to(f(\mathsf{lim}(x))\sim_{\epsilon/2}f(v))$ $\displaystyle(\mathsf{lim}(x)\sim_{\eta}v)$ $\displaystyle\to(g(\mathsf{lim}(x))\sim_{\epsilon/2}g(v)).$

Choosing $\delta<\min(\theta,\eta)$, by \autorefthm:RC-sim-lim-term we have both $\mathsf{lim}(x)\sim_{\theta}y_{\delta}$ and $\mathsf{lim}(x)\sim_{\eta}y_{\delta}$. Hence

 $f(\mathsf{lim}(x))\sim_{\epsilon/2}f(y_{\delta})=g(y_{\delta})\sim_{\epsilon/2% }g(\mathsf{lim}(x))$

and thus $f(\mathsf{lim}(x))\sim_{\epsilon}g(\mathsf{lim}(x))$ by the triangle inequality. β

 Title 11.3.2 Induction and recursion on Cauchy reals \metatable