11.3.2 Induction and recursion on Cauchy reals

In order to do anything useful with ${ℝ}_{𝖼}$, 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 ${ℝ}_{𝖼}$ and $\mathrm{\sim }$ requires a simultaneous induction over both at once.Thus, we should expect it to say that assuming two type families over ${ℝ}_{𝖼}$ and $\mathrm{\sim }$, respectively, together with data corresponding to each constructor, there exist sections of both of these families.However, since $\mathrm{\sim }$ is indexed on two copies of ${ℝ}_{𝖼}$, the precise dependencies of these families is a bit subtle.The induction principle will apply to any pair of type families:

$A$$:{ℝ}_{𝖼}\to 𝒰$

$B$$:{\displaystyle \prod _{x,y:{ℝ}_{𝖼}}}A(x)\to A(y)\to {\displaystyle \prod _{ϵ:{\mathbb{Q}}_{+}}}(x{\sim }_{ϵ}y)\to 𝒰.$

The type of $A$ is obvious, but the type of $B$ requires a little thought.Since $B$ must depend on $\mathrm{\sim }$, but $\mathrm{\sim }$ in turn depends on two copies of ${ℝ}_{𝖼}$ and one copy of ${\mathbb{Q}}_{+}$, it is fairly obvious that $B$ must also depend on the variables $x,y:{ℝ}_{𝖼}$ and $ϵ:{\mathbb{Q}}_{+}$ as well as an element of $(x{\sim }_{ϵ}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:{ℝ}_{𝖼}$ or $x{\sim }_{ϵ}y$.But the recursion principle (along with its associated uniqueness principle) is supposed to say that ${ℝ}_{𝖼}$ with ${\sim }_{ϵ}$ is an “initial object” in some category, so in this case the dependency structure of $A$ and $B$ should mirror that of ${ℝ}_{𝖼}$ and ${\sim }_{ϵ}$: that is, we should have $B:A\to A\to {\mathbb{Q}}_{+}\to 𝒰$.Combining this observation with the fact that, in the dependent case, $B$ must also depend on $x,y:{ℝ}_{𝖼}$ and $x{\sim }_{ϵ}y$, leads inevitably to the type given above for $B$.

It is helpful to think of $B$ as an $ϵ$-indexed family of relations between the types $A(x)$ and $A(y)$.With this in mind, we may write $B(x,y,a,b,ϵ,\xi )$ as $(x,a){⌢}_{ϵ}^{\xi }(y,b)$.Since $\xi :x{\sim }_{ϵ}y$ is unique when it exists, we generally omit it from the notation and write $(x,a){⌢}_{ϵ}(y,b)$; this is harmless as long as we keep in mind that this relation is only defined when $x{\sim }_{ϵ}y$.We may also sometimes simplify further and write $a{⌢}_{ϵ}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:{ℝ}_{𝖼}\to 𝒰$ and a family of relations $⌢$ as above, the hypotheses of the induction principle consist of the following data, one for each constructor of ${ℝ}_{𝖼}$ or $\mathrm{\sim }$:

• For any $q:\mathbb{Q}$, an element $f_q:A(\mathrm{𝗋𝖺𝗍}(q))$.

• For any Cauchy approximation $x$, and any $a:{\prod }_{(ϵ:{\mathbb{Q}}_{+})}A(x_{ϵ})$ such that

  $$\forall (\delta ,ϵ:{\mathbb{Q}}_{+}).(x_{\delta },a_{\delta }){⌢}_{\delta +ϵ}(x_{ϵ},a_{ϵ}),$$(11.3.1)

  an element $f_{x,a}:A(\mathrm{𝗅𝗂𝗆}(x))$.We call such $a$ a dependent Cauchy approximationover $x$.

• For $u,v:{ℝ}_{𝖼}$ such that $h:\forall (ϵ:{\mathbb{Q}}_{+}).u{\sim }_{ϵ}v$, and all $a:A(u)$ and $b:A(v)$ such that$\forall (ϵ:{\mathbb{Q}}_{+}).(u,a){⌢}_{ϵ}(v,b)$,a dependent path $a{=}_{{\mathrm{𝖾𝗊}}_{{ℝ}_{𝖼}}(u,v)}^{A}b$.

• For $q,r:\mathbb{Q}$ and $ϵ:{\mathbb{Q}}_{+}$, if , we have$(\mathrm{𝗋𝖺𝗍}(q),f_q){⌢}_{ϵ}(\mathrm{𝗋𝖺𝗍}(r),f_r).$

• For $q:\mathbb{Q}$ and $\delta ,ϵ:{\mathbb{Q}}_{+}$ and $y$ a Cauchy approximation, and $b$ a dependent Cauchy approximation over $y$, if $\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ-\delta }{y}_{\delta }$, then

  $$(\mathrm{𝗋𝖺𝗍}(q),f_q){⌢}_{ϵ-\delta }(y_{\delta },b_{\delta })\Rightarrow (\mathrm{𝗋𝖺𝗍}(q),f_q){⌢}_{ϵ}(\mathrm{𝗅𝗂𝗆}(y),f_{y,b}).$$

• Similarly, for $r:\mathbb{Q}$ and $\delta ,ϵ:{\mathbb{Q}}_{+}$ and $x$ a Cauchy approximation, and $a$ a dependent Cauchy approximation over $x$, if $x_{\delta }{\sim }_{ϵ-\delta }\mathrm{𝗋𝖺𝗍}(r)$, then

  $$(x_{\delta },a_{\delta }){⌢}_{ϵ-\delta }(\mathrm{𝗋𝖺𝗍}(r),f_r)\Rightarrow (\mathrm{𝗅𝗂𝗆}(x),f_{x,a}){⌢}_{ϵ}(\mathrm{𝗋𝖺𝗍}(q),f_r).$$

• For $ϵ,\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 }_{ϵ-\delta -\eta }{y}_{\eta }$, then

  $$(x_{\delta },a_{\delta }){⌢}_{ϵ-\delta -\eta }(y_{\eta },b_{\eta })\Rightarrow (\mathrm{𝗅𝗂𝗆}(x),f_{x,a}){⌢}_{ϵ}(\mathrm{𝗅𝗂𝗆}(y),f_{y,b}).$$

• For $ϵ:{\mathbb{Q}}_{+}$ and $x,y:{ℝ}_{𝖼}$ and $\xi ,\zeta :x{\sim }_{ϵ}y$, and $a:A(x)$ and $b:A(y)$, any two elements of $(x,a){⌢}_{ϵ}^{\xi }(y,b)$ and $(x,a){⌢}_{ϵ}^{\zeta }(y,b)$ are dependently equal over $\xi =\zeta$.Note that as usual, this is equivalent to asking that $⌢$ takes values in mere propositions.

Under these hypotheses, we deduce functions

$f$$:{\displaystyle \prod _{x:{ℝ}_{𝖼}}}A(x)$

$g$$:{\displaystyle \prod _{(x,y:{ℝ}_{𝖼})}}{\displaystyle \prod _{(ϵ:{\mathbb{Q}}_{+})}}{\displaystyle \prod _{(\xi :x{\sim }_{ϵ}y)}}(x,f(x)){⌢}_{ϵ}^{\xi }(y,f(y))$

which compute as expected:

$f(\mathrm{𝗋𝖺𝗍}(q))$$:\equiv f_q,$(11.3.2)

$f(\mathrm{𝗅𝗂𝗆}(x))$$:\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]}_{ϵ}:\equiv f(x_{ϵ}):A(x_{ϵ})$, and then for any $ϵ,\delta :{\mathbb{Q}}_{+}$ we have $g(x_{ϵ},x_{\delta },ϵ+\delta ,\xi )$ to witness the fact that $(f,g)[x]$ is a dependent Cauchy approximation, where $\xi :x_{ϵ}{\sim }_{ϵ+\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_{ϵ})$ 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 ${ℝ}_{𝖼}$ and for $\mathrm{\sim }$.Firstly, suppose given only a type family $A:{ℝ}_{𝖼}\to 𝒰$, and define $⌢$ to be constant at $\mathrm{𝟏}$.Then much of the required data becomes trivial, and we are left with:

• for any $q:\mathbb{Q}$, an element $f_q:A(\mathrm{𝗋𝖺𝗍}(q))$,

• for any Cauchy approximation $x$, and any $a:{\prod }_{(ϵ:{\mathbb{Q}}_{+})}A(x_{ϵ})$, an element $f_{x,a}:A(\mathrm{𝗅𝗂𝗆}(x))$,

• for $u,v:{ℝ}_{𝖼}$ and $h:\forall (ϵ:{\mathbb{Q}}_{+}).u{\sim }_{ϵ}v$, and $a:A(u)$ and $b:A(v)$, we have $a{=}_{{\mathrm{𝖾𝗊}}_{{ℝ}_{𝖼}}(u,v)}^{A}b$.

Given these data, the induction principle yields a function $f:{\prod }_{(x:{ℝ}_{𝖼})}A(x)$ such that

$f(\mathrm{𝗋𝖺𝗍}(q))$$:\equiv f_q,$

$f(\mathrm{𝗅𝗂𝗆}(x))$$:\equiv f_{x,f(x)}.$

We call this principle ${ℝ}_{𝖼}$-induction; it says essentially that if we take ${\sim }_{ϵ}$ as given, then ${ℝ}_{𝖼}$ is inductively generated by its constructors.

In particular, if $A$ is a mere property, the third hypothesis in ${ℝ}_{𝖼}$-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\mathrm{:}{\mathrm{R}}_{\mathrm{c}}$ and $ϵ\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}$, we have $u{\mathrm{\sim }}_{ϵ}u$.

Proof.

Define $A(u):\equiv \forall (ϵ:{\mathbb{Q}}_{+}).(u{\sim }_{ϵ}u)$.Since this is a mere proposition (by the last constructor of $\mathrm{\sim }$), by ${ℝ}_{𝖼}$-induction, it suffices to prove it when $u$ is $\mathrm{𝗋𝖺𝗍}(q)$ and when $u$ is $\mathrm{𝗅𝗂𝗆}(x)$.In the first case, we obviously have for any $ϵ$, hence $\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ}\mathrm{𝗋𝖺𝗍}(q)$ by the first constructor of $\mathrm{\sim }$.And in the second case, we may assume inductively that $x_{\delta }{\sim }_{ϵ}{x}_{\delta }$ for all $\delta ,ϵ:{\mathbb{Q}}_{+}$.Then in particular, we have $x_{ϵ/3}{\sim }_{ϵ/3}{x}_{ϵ/3}$, whence $\mathrm{𝗅𝗂𝗆}(x){\sim }_{ϵ}\mathrm{𝗅𝗂𝗆}(x)$ by the fourth constructor of $\mathrm{\sim }$.∎

Theorem 11.3.3.

${ℝ}_{𝖼}$ is a set.

Proof.

We have just shown that the mere relation$P(u,v):\equiv \forall (ϵ:{\mathbb{Q}}_{+}).(u{\sim }_{ϵ}v)$is reflexive.Since it implies identity, by the path constructor of ${ℝ}_{𝖼}$, the result follows from thm:h-set-refrel-in-paths-sets.∎

We can also show that although ${ℝ}_{𝖼}$ 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 ${ℝ}_{𝖼}$, but it is a useful property.)We define the type of Cauchy approximations to be

$$𝒞:\equiv x:{\mathbb{Q}}_{+}\to {ℝ}_{𝖼}|\forall (ϵ,\delta :{\mathbb{Q}}_{+}).x_{\delta }{\sim }_{\delta +ϵ}{x}_{ϵ}.$$

The second constructor of ${ℝ}_{𝖼}$ gives a function $\mathrm{𝗅𝗂𝗆}:𝒞\to {ℝ}_{𝖼}$.

Lemma 11.3.4.

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

Proof.

By ${ℝ}_{𝖼}$-induction, we may divide into cases on $u$.Of course, if $u$ is a limit $\mathrm{𝗅𝗂𝗆}(x)$, the statement is trivial.So suppose $u$ is a rational point $\mathrm{𝗋𝖺𝗍}(q)$; we claim $u$ is equal to $\mathrm{𝗅𝗂𝗆}(\lambda ϵ.\mathrm{𝗋𝖺𝗍}(q))$.By the path constructor of ${ℝ}_{𝖼}$, it suffices to show $\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ}\mathrm{𝗅𝗂𝗆}(\lambda ϵ.\mathrm{𝗋𝖺𝗍}(q))$ for all $ϵ:{\mathbb{Q}}_{+}$.And by the second constructor of $\mathrm{\sim }$, for this it suffices to find $\delta :{\mathbb{Q}}_{+}$ such that $\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ-\delta }\mathrm{𝗋𝖺𝗍}(q)$.But by the first constructor of $\mathrm{\sim }$, we may take any $\delta :{\mathbb{Q}}_{+}$ with .∎

Lemma 11.3.5.

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

$$\forall (x,y:𝒞).\mathrm{𝗅𝗂𝗆}(x)=\mathrm{𝗅𝗂𝗆}(y)\Rightarrow f(x)=f(y),$$

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

Proof.

Since $\mathrm{𝗅𝗂𝗆}$ is surjective, by lem:images_are_coequalizers, ${ℝ}_{𝖼}$ is the quotient of $𝒞$ by the kernel pair of $\mathrm{𝗅𝗂𝗆}$.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 $\mathrm{𝟏}$.In this case, $⌢$ is simply an $ϵ$-indexed family of relations on $ϵ$-close pairs of real numbers, so we may write $u{⌢}_{ϵ}v$ instead of $(u,\star ){⌢}_{ϵ}(v,\star )$.Then the required data reduces to the following, where $q,r$ denote rational numbers, $ϵ,\delta ,\eta$ positive rational numbers, and $x,y$ Cauchy approximations:

• if , then$\mathrm{𝗋𝖺𝗍}(q){⌢}_{ϵ}\mathrm{𝗋𝖺𝗍}(r)$,

• if $\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ-\delta }{y}_{\delta }$ and$\mathrm{𝗋𝖺𝗍}(q){⌢}_{ϵ-\delta }{y}_{\delta }$,then $\mathrm{𝗋𝖺𝗍}(q){⌢}_{ϵ}\mathrm{𝗅𝗂𝗆}(y)$,

• if $x_{\delta }{\sim }_{ϵ-\delta }\mathrm{𝗋𝖺𝗍}(r)$ and$x_{\delta }{⌢}_{ϵ-\delta }\mathrm{𝗋𝖺𝗍}(r)$,then $\mathrm{𝗅𝗂𝗆}(y){⌢}_{ϵ}\mathrm{𝗋𝖺𝗍}(q)$,

• if $x_{\delta }{\sim }_{ϵ-\delta -\eta }{y}_{\eta }$ and$x_{\delta }{⌢}_{ϵ-\delta -\eta }{y}_{\eta }$,then $\mathrm{𝗅𝗂𝗆}(x){⌢}_{ϵ}\mathrm{𝗅𝗂𝗆}(y)$.

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

Lemma 11.3.6.

For any $u\mathrm{,}v\mathrm{:}{\mathrm{R}}_{\mathrm{c}}$ and $ϵ\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}$, we have $\mathrm{(}u{\mathrm{\sim }}_{ϵ}v\mathrm{)}\mathrm{=}\mathrm{(}v{\mathrm{\sim }}_{ϵ}u\mathrm{)}$.

Proof.

Since both are mere propositions, by symmetry it suffices to show one implication.Thus, let $(u{⌢}_{ϵ}v):\equiv (v{\sim }_{ϵ}u)$.By $\mathrm{\sim }$-induction, we may reduce to the case that $u{\sim }_{ϵ}v$ is derived from one of the four interesting constructors of $\mathrm{\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 $\mathrm{\sim }$ (the second and third constructors switch, while the fourth stays put).∎

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

1. for every $q:\mathbb{Q}$ construct $f(\mathrm{𝗋𝖺𝗍}(q)):A$,

2. for every Cauchy approximation $x:{\mathbb{Q}}_{+}\to {ℝ}_{𝖼}$, construct $f(x):A$,assuming that $f(x_{ϵ})$ has already been defined for all $ϵ:{\mathbb{Q}}_{+}$,

3. prove $f(u)=f(v)$ for all $u,v:{ℝ}_{𝖼}$ satisfying $\forall (ϵ:{\mathbb{Q}}_{+}).u{\sim }_{ϵ}v$.

However, it is generally quite difficult to show 3 without knowing something about how $f$ acts on $ϵ$-close Cauchy reals.The enhanced principle of $({ℝ}_{𝖼},\mathrm{\sim })$-recursion remedies this deficiency, allowing us to specify an arbitrary “way in which $f$ acts on $ϵ$-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 $⌢$.Since $A$ is independent of ${ℝ}_{𝖼}$, we may assume for simplicity that $⌢$ depends only on $A$ and ${\mathbb{Q}}_{+}$, and thus there is no ambiguity in writing $a{⌢}_{ϵ}b$ instead of $(u,a){⌢}_{ϵ}(v,b)$.In this case, defining a function $f:{ℝ}_{𝖼}\to A$ by $({ℝ}_{𝖼},\mathrm{\sim })$-recursion requires the following cases (which we now write using the pattern-matching convention).

• For every $q:\mathbb{Q}$, construct $f(\mathrm{𝗋𝖺𝗍}(q)):A$.

• For every Cauchy approximation $x:{\mathbb{Q}}_{+}\to {ℝ}_{𝖼}$, construct $f(x):A$, assuming inductively that $f(x_{ϵ})$ has already been defined for all $ϵ:{\mathbb{Q}}_{+}$ and form a “Cauchy approximation with respect to $⌢$”, i.e. that $\forall (ϵ,\delta :{\mathbb{Q}}_{+}).(f(x_{ϵ}){⌢}_{ϵ+\delta }f(x_{\delta }))$.

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

• Prove that if for $q,r:\mathbb{Q}$, then $f(\mathrm{𝗋𝖺𝗍}(q)){⌢}_{ϵ}f(\mathrm{𝗋𝖺𝗍}(r))$.

• For any $q:\mathbb{Q}$ and any Cauchy approximation $y$, prove that$f(\mathrm{𝗋𝖺𝗍}(q)){⌢}_{ϵ}f(\mathrm{𝗅𝗂𝗆}(y)),$ assuming inductively that $\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ-\delta }{y}_{\delta }$ and $f(\mathrm{𝗋𝖺𝗍}(q)){⌢}_{ϵ-\delta }f(y_{\delta })$ for some $\delta :{\mathbb{Q}}_{+}$, and that $\eta \mapsto f(x_{\eta })$ is a Cauchy approximation with respect to $⌢$.

• For any Cauchy approximation $x$ and any $r:\mathbb{Q}$, prove that$f(\mathrm{𝗅𝗂𝗆}(x)){⌢}_{ϵ}f(\mathrm{𝗋𝖺𝗍}(r)),$assuming inductively that $x_{\delta }{\sim }_{ϵ-\delta }\mathrm{𝗋𝖺𝗍}(r)$ and $f(x_{\delta }){⌢}_{ϵ-\delta }f(\mathrm{𝗋𝖺𝗍}(r))$ for some $\delta :{\mathbb{Q}}_{+}$, and that $\eta \mapsto f(x_{\eta })$ is a Cauchy approximation with respect to $⌢$.

• For any Cauchy approximations $x,y$, prove that$f(\mathrm{𝗅𝗂𝗆}(x)){⌢}_{ϵ}f(\mathrm{𝗅𝗂𝗆}(y)),$assuming inductively that $x_{\delta }{\sim }_{ϵ-\delta -\eta }{y}_{\eta }$ and $f(x_{\delta }){⌢}_{ϵ-\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 $⌢$.

Note that in the last four proofs, we are free to use the specific definitions of $f(\mathrm{𝗋𝖺𝗍}(q))$ and $f(\mathrm{𝗅𝗂𝗆}(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 $⌢$.Thus, we often verify it first, immediately after defining $⌢$, before going on to define $f(\mathrm{𝗋𝖺𝗍}(q))$ and $f(\mathrm{𝗅𝗂𝗆}(x))$.

Under the above hypotheses, $({ℝ}_{𝖼},\mathrm{\sim })$-recursion yields a function $f:{ℝ}_{𝖼}\to A$ such that $f(\mathrm{𝗋𝖺𝗍}(q))$ and $f(\mathrm{𝗅𝗂𝗆}(x))$ are judgmentally equal to the definitions given for them in the first two clauses.Moreover, we may also conclude

$$\forall (u,v:{ℝ}_{𝖼}).\forall (ϵ:{\mathbb{Q}}_{+}).(u{\sim }_{ϵ}v)\to (f(u){⌢}_{ϵ}f(v)).$$(11.3.7)

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

Definition 11.3.8.

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

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

$$(u{\sim }_{ϵ}v)\Rightarrow (g(u){\sim }_{Lϵ}g(v))$$

for all $ϵ\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}$ and $u\mathrm{,}v\mathrm{:}{\mathrm{R}}_{\mathrm{c}}$..

In particular, note that by the first constructor of $\mathrm{\sim }$, if $f:\mathbb{Q}\to \mathbb{Q}$ is Lipschitz in the obvious sense, then so is the composite $\mathbb{Q}\stackrel{𝑓}{\to }\mathbb{Q}\to {ℝ}_{𝖼}$.

Lemma 11.3.9.

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

Proof.

We define $\overline{f}$ by $({ℝ}_{𝖼},\mathrm{\sim })$-recursion, with codomain $A:\equiv {ℝ}_{𝖼}$.We define the relation $\mathrm{⌢}:{ℝ}_{𝖼}\to {ℝ}_{𝖼}\to {\mathbb{Q}}_{+}\to \mathrm{𝖯𝗋𝗈𝗉}$ to be

$(u{⌢}_{ϵ}v)$$:\equiv (u{\sim }_{Lϵ}v).$

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

$$\overline{f}(\mathrm{𝗋𝖺𝗍}(q)):\equiv \mathrm{𝗋𝖺𝗍}(f(q)).$$

For a Cauchy approximation $x:{\mathbb{Q}}_{+}\to {ℝ}_{𝖼}$, we define

$$\overline{f}(\mathrm{𝗅𝗂𝗆}(x)):\equiv \mathrm{𝗅𝗂𝗆}(\lambda ϵ.\overline{f}(x_{ϵ/L})).$$

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

$$y_{\delta }\equiv f(x_{\delta /L}){\sim }_{\delta +ϵ}f(x_{ϵ/L})\equiv y_{ϵ}.$$

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

To complete the $({ℝ}_{𝖼},\mathrm{\sim })$-recursion, it remains to verify the four conditions on $⌢$.This basically amounts to proving that $\overline{f}$ is Lipschitz for all the four constructors of $\mathrm{\sim }$.

1. When $u$ is $\mathrm{𝗋𝖺𝗍}(q)$ and $v$ is $\mathrm{𝗋𝖺𝗍}(r)$ with , the assumption that $f$ is Lipschitz yields $f(q){\sim }_{Lϵ}f(r)$, hence $\overline{f}(\mathrm{𝗋𝖺𝗍}(q)){⌢}_{ϵ}\overline{f}(\mathrm{𝗋𝖺𝗍}(r))$ by definition.

2. When $u$ is $\mathrm{𝗅𝗂𝗆}(x)$ and $v$ is $\mathrm{𝗋𝖺𝗍}(q)$ with $x_{\eta }{\sim }_{ϵ-\eta }\mathrm{𝗋𝖺𝗍}(q)$, then theinductive hypothesis is $\overline{f}(x_{\eta }){\sim }_{Lϵ-L\eta }\mathrm{𝗋𝖺𝗍}(f(q))$, which proves$\overline{f}(\mathrm{𝗅𝗂𝗆}(x)){\sim }_{Lϵ}\overline{f}(\mathrm{𝗋𝖺𝗍}(q))$by the third constructor of $\mathrm{\sim }$.

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

4. When $u$ is $\mathrm{𝗅𝗂𝗆}(x)$ and $v$ is $\mathrm{𝗅𝗂𝗆}(y)$, with $\delta ,\eta :{\mathbb{Q}}_{+}$ such that $x_{\delta }{\sim }_{ϵ-\delta -\eta }{y}_{\eta }$,the inductive hypothesis is $\overline{f}(x_{\delta }){\sim }_{Lϵ-L\delta -L\eta }\overline{f}(y_{\eta })$, which proves $\overline{f}(\mathrm{𝗅𝗂𝗆}(x)){\sim }_{Lϵ}\overline{f}(\mathrm{𝗅𝗂𝗆}(y))$ by the fourth constructor of $\mathrm{\sim }$.

This completes the $({ℝ}_{𝖼},\mathrm{\sim })$-recursion, and hence the construction of $\overline{f}$.The desired equality $\overline{f}(\mathrm{𝗋𝖺𝗍}(q))\equiv f(q)$ is exactly the first computation rule for $({ℝ}_{𝖼},\mathrm{\sim })$-recursion, and the additional condition (11.3.7) says exactly that $\overline{f}$ is Lipschitz with constant $L$.∎

At this point we have gone about as far as we can without a better characterization of $\mathrm{\sim }$.We have specified, in the constructors of $\mathrm{\sim }$, the conditions under which we want Cauchy reals of the two different forms to be $ϵ$-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 sec: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 $\mathrm{\sim }$ more precisely, we will define a family of relations ${\approx }_{ϵ}$ on ${ℝ}_{𝖼}$ recursively, so that they will compute on constructors, and prove that this family is equivalent to ${\sim }_{ϵ}$.

Theorem 11.3.10.

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

$(\mathrm{𝗋𝖺𝗍}(q){\approx }_{ϵ}\mathrm{𝗋𝖺𝗍}(r))$(11.3.10)

$(\mathrm{𝗋𝖺𝗍}(q){\approx }_{ϵ}\mathrm{𝗅𝗂𝗆}(y))$$:\equiv \exists (\delta :{\mathbb{Q}}_{+}).\mathrm{𝗋𝖺𝗍}(q){\approx }_{ϵ-\delta }{y}_{\delta }$(11.3.10)

$(\mathrm{𝗅𝗂𝗆}(x){\approx }_{ϵ}\mathrm{𝗋𝖺𝗍}(r))$$:\equiv \exists (\delta :{\mathbb{Q}}_{+}).x_{\delta }{\approx }_{ϵ-\delta }\mathrm{𝗋𝖺𝗍}(r)$(11.3.10)

$(\mathrm{𝗅𝗂𝗆}(x){\approx }_{ϵ}\mathrm{𝗅𝗂𝗆}(y))$$:\equiv \exists (\delta ,\eta :{\mathbb{Q}}_{+}).x_{\delta }{\approx }_{ϵ-\delta -\eta }{y}_{\eta }.$(11.3.10)

Moreover, we have

$$(u{\approx }_{ϵ}v)\iff \exists (\theta :{\mathbb{Q}}_{+}).(u{\approx }_{ϵ-\theta }v)$$(11.3.10)

$$(u{\approx }_{ϵ}v)\to (v{\sim }_{\delta }w)\to (u{\approx }_{ϵ+\delta }w)$$(11.3.10)

$$(u{\sim }_{ϵ}v)\to (v{\approx }_{\delta }w)\to (u{\approx }_{ϵ+\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$,

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

Conditions (11.3.10) and (11.3.10) are forms of the triangle inequality, which say that $\approx$ is a “module” over $\mathrm{\sim }$ on both sides.

Proof.

We will define $\mathrm{\approx }:{ℝ}_{𝖼}\to {ℝ}_{𝖼}\to {\mathbb{Q}}_{+}\to \mathrm{𝖯𝗋𝗈𝗉}$ by double $({ℝ}_{𝖼},\mathrm{\sim })$-recursion.First we will apply $({ℝ}_{𝖼},\mathrm{\sim })$-recursion with codomain the subset of ${ℝ}_{𝖼}\to {\mathbb{Q}}_{+}\to \mathrm{𝖯𝗋𝗈𝗉}$ 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,ϵ)\mapsto (\mathrm{♢}{\approx }_{ϵ}u)$, with the symbol $\mathrm{♢}$ referring to the whole relation.Now we can write $A$ precisely as

$$\begin{array}{c}A:\equiv \{\mathrm{♢}:{ℝ}_{𝖼}\to {\mathbb{Q}}_{+}\to \mathrm{𝖯𝗋𝗈𝗉}|\hfill \\ \hfill (\forall (u:{ℝ}_{𝖼}).\forall (ϵ:{\mathbb{Q}}_{+}).((\mathrm{♢}{\approx }_{ϵ}u)\iff \exists (\theta :{\mathbb{Q}}_{+}).(\mathrm{♢}{\approx }_{ϵ-\theta }u)))\\ \hfill \wedge (\forall (u,v:{ℝ}_{𝖼}).\forall (\eta ,ϵ:{\mathbb{Q}}_{+}).(u{\sim }_{ϵ}v)\to \\ \hfill ((\mathrm{♢}{\approx }_{\eta }u)\to (\mathrm{♢}{\approx }_{\eta +ϵ}v))\wedge ((\mathrm{♢}{\approx }_{\eta }v)\to (\mathrm{♢}{\approx }_{\eta +ϵ}u)))\}\end{array}$$

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

$$(\mathrm{♢}{⌢}_{ϵ}\mathrm{♡}):\equiv \forall (u:{ℝ}_{𝖼}).\forall (\eta :{\mathbb{Q}}_{+}).((\mathrm{♢}{\approx }_{\eta }u)\to (\mathrm{♡}{\approx }_{ϵ+\eta }u))\wedge ((\mathrm{♡}{\approx }_{\eta }u)\to (\mathrm{♢}{\approx }_{ϵ+\eta }u)).$$

We observe that these relations are separated.For assuming$\forall (ϵ:{\mathbb{Q}}_{+}).(\mathrm{♢}{⌢}_{ϵ}\mathrm{♡}),$to show $\mathrm{♢}=\mathrm{♡}$ it suffices to show $(\mathrm{♢}{\approx }_{ϵ}u)\iff (\mathrm{♡}{\approx }_{ϵ}u)$ for all $u:{ℝ}_{𝖼}$.But $\mathrm{♢}{\approx }_{ϵ}u$ implies $\mathrm{♢}{\approx }_{ϵ-\theta }u$ for some $\theta$, by roundedness, which together with $\mathrm{♢}{⌢}_{ϵ}\mathrm{♡}$ implies $\mathrm{♡}{\approx }_{ϵ}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 $(\mathrm{𝗋𝖺𝗍}(q){\approx }_{(\text{–})}\text{–})$.

• For any Cauchy approximation $x$, if we assume defined a function ${\mathbb{Q}}_{+}\to A$, which we will denote by $ϵ\mapsto (x_{ϵ}{\approx }_{(\text{–})}\text{–})$, with the property that

  $$\forall (u:{ℝ}_{𝖼}).\forall (\delta ,ϵ,\eta :{\mathbb{Q}}_{+}).(x_{\delta }{\approx }_{\eta }u)\to (x_{ϵ}{\approx }_{\eta +\delta +ϵ}u),$$(11.3.11)

  we must give an element of $A$, which we write as $(\mathrm{𝗅𝗂𝗆}(x){\approx }_{(\text{–})}\text{–})$.

In both cases, we give the required definition by using a nested $({ℝ}_{𝖼},\mathrm{\sim })$-recursion, with codomain the subset of ${\mathbb{Q}}_{+}\to \mathrm{𝖯𝗋𝗈𝗉}$ consisting of rounded families of mere propositions.Thinking of these propositions as zero halves of a binary relation, we will write them as $ϵ\mapsto (\bullet {\approx }_{ϵ}\mathrm{△})$, with the symbol $\mathrm{△}$ referring to the whole family.Now we can write the codomain of these inner recursions precisely as

$$C:\equiv \{\mathrm{△}:{\mathbb{Q}}_{+}\to \mathrm{𝖯𝗋𝗈𝗉}|\forall (ϵ:{\mathbb{Q}}_{+}).((\bullet {\approx }_{ϵ}\mathrm{△})\iff \exists (\theta :{\mathbb{Q}}_{+}).(\bullet {\approx }_{ϵ-\theta }\mathrm{△}))\}$$

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

$$(\mathrm{△}{⌣}_{ϵ}\mathrm{\square }):\equiv \forall (\eta :{\mathbb{Q}}_{+}).((\bullet {\approx }_{\eta }\mathrm{△})\to (\bullet {\approx }_{ϵ+\eta }\mathrm{\square }))\wedge ((\bullet {\approx }_{\eta }\mathrm{\square })\to (\bullet {\approx }_{ϵ+\eta }\mathrm{△})).$$

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

Note that if such an inner recursion succeeds, it will yield a family of predicates $\mathrm{♢}:{ℝ}_{𝖼}\to {\mathbb{Q}}_{+}\to \mathrm{𝖯𝗋𝗈𝗉}$ which are rounded(since their image in ${\mathbb{Q}}_{+}\to \mathrm{𝖯𝗋𝗈𝗉}$ lies in $C$) and satisfy

$$\forall (u,v:{ℝ}_{𝖼}).\forall (ϵ:{\mathbb{Q}}_{+}).(u{\sim }_{ϵ}v)\to \left((\mathrm{♢}{\approx }_{(\text{–})}u){⌣}_{ϵ}(\mathrm{♢}{\approx }_{(\text{–})}u)\right).$$

Expanding out the definition of $⌣$, this yields precisely the third condition for $\mathrm{♢}$ 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 $(\mathrm{𝗋𝖺𝗍}(q){\approx }_{(\text{–})}{y}_{\delta }):C$, while in (11.3.10) and (11.3.10) it is that $(x_{\delta }{\approx }_{(\text{–})}\text{–}):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 $\mathrm{\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 $\mathrm{𝗋𝖺𝗍}(q)$.

1. Assuming $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi }\mathrm{𝗋𝖺𝗍}(r)$ and , we must show $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi +ϵ}\mathrm{𝗋𝖺𝗍}(s)$.But by definition of $\approx$, this reduces to the triangle inequality for rational numbers.

2. We assume $\varphi ,ϵ,\delta :{\mathbb{Q}}_{+}$ such that $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi }\mathrm{𝗋𝖺𝗍}(r)$ and $\mathrm{𝗋𝖺𝗍}(r){\sim }_{ϵ-\delta }{y}_{\delta }$, and inductively that

   $$\forall (\psi :{\mathbb{Q}}_{+}).(\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi }\mathrm{𝗋𝖺𝗍}(r))\to (\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi +ϵ-\delta }{y}_{\delta }).$$(11.3.12)

   We assume also that $\psi ,\delta \mapsto (\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi }{y}_{\delta })$ is a Cauchy approximation with respect to $⌣$, i.e.

   $$\forall (\psi ,\xi ,\zeta :{\mathbb{Q}}_{+}).(\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi }{y}_{\xi })\to (\mathrm{𝗋𝖺𝗍}(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 \varphi$ yields immediately $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi +ϵ-\delta }{y}_{\delta }$, and hence $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi +ϵ}\mathrm{𝗅𝗂𝗆}(y)$ by definition of $\approx$.

3. We assume $\varphi ,ϵ,\delta :{\mathbb{Q}}_{+}$ such that $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi }\mathrm{𝗅𝗂𝗆}(y)$ and $y_{\delta }{\sim }_{ϵ-\delta }\mathrm{𝗋𝖺𝗍}(r)$, and inductively that

   $$\forall (\psi :{\mathbb{Q}}_{+}).(\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi }{y}_{\delta })\to (\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi +ϵ-\delta }\mathrm{𝗋𝖺𝗍}(r)).$$(11.3.14)

   $$\forall (\psi ,\xi ,\zeta :{\mathbb{Q}}_{+}).(\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi }{y}_{\xi })\to (\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi +\xi +\zeta }{y}_{\zeta }).$$(11.3.14)

   By definition, $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi }\mathrm{𝗅𝗂𝗆}(y)$ means that we have $\theta :{\mathbb{Q}}_{+}$ with $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi -\theta }{y}_{\theta }$.By assumption (11.3.14), therefore, we have also $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi +\delta }{y}_{\delta }$, and then by (11.3.14) it follows that $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi +ϵ}\mathrm{𝗋𝖺𝗍}(r)$, as desired.

4. We assume $\varphi ,ϵ,\delta ,\eta :{\mathbb{Q}}_{+}$ such that $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi }\mathrm{𝗅𝗂𝗆}(y)$ and $y_{\delta }{\sim }_{ϵ-\delta -\eta }{z}_{\eta }$, and inductively that

   $$\forall (\psi :{\mathbb{Q}}_{+}).(\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi }{y}_{\delta })\to (\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi +ϵ-\delta -\eta }{z}_{\eta }),$$(11.3.14)

   $$\forall (\psi ,\xi ,\zeta :{\mathbb{Q}}_{+}).(\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi }{y}_{\xi })\to (\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi +\xi +\zeta }{y}_{\zeta }),$$(11.3.14)

   $$\forall (\psi ,\xi ,\zeta :{\mathbb{Q}}_{+}).(\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi }{z}_{\xi })\to (\mathrm{𝗋𝖺𝗍}(q){\approx }_{\psi +\xi +\zeta }{z}_{\zeta }).$$(11.3.14)

   Again, $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi }\mathrm{𝗅𝗂𝗆}(y)$ means we have $\xi :{\mathbb{Q}}_{+}$ with $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi -\xi }{y}_{\xi }$, while (11.3.14) then implies $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi +\delta }{y}_{\delta }$ and (11.3.14) implies $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi +ϵ-\eta }{z}_{\eta }$.But by definition of $\approx$, this implies $\mathrm{𝗋𝖺𝗍}(q){\approx }_{\varphi +ϵ}\mathrm{𝗅𝗂𝗆}(z)$ as desired.

Now we move on to the cases when $u$ is $\mathrm{𝗅𝗂𝗆}(x)$, with $x$ a Cauchy approximation.In this case, the ambient inductive hypothesis of the definition of $(\mathrm{𝗅𝗂𝗆}(x){\approx }_{(\text{–})}\text{–}):A$ is that we have $(x_{\delta }{\approx }_{(\text{–})}\text{–}):A$, so that in addition to being rounded they satisfy the triangle inequality on the right.

1. Assuming $\mathrm{𝗅𝗂𝗆}(x){\approx }_{\varphi }\mathrm{𝗋𝖺𝗍}(r)$ and , we must show $\mathrm{𝗅𝗂𝗆}(x){\approx }_{\varphi +ϵ}\mathrm{𝗋𝖺𝗍}(s)$.By definition of $\approx$, the former means $x_{\delta }{\approx }_{\varphi -\delta }\mathrm{𝗋𝖺𝗍}(r)$, so that above triangle inequality implies $x_{\delta }{\approx }_{ϵ+\varphi -\delta }\mathrm{𝗋𝖺𝗍}(s)$, hence $\mathrm{𝗅𝗂𝗆}(x){\approx }_{\varphi +ϵ}\mathrm{𝗋𝖺𝗍}(s)$ as desired.

2. We assume $\varphi ,ϵ,\delta :{\mathbb{Q}}_{+}$ such that $\mathrm{𝗅𝗂𝗆}(x){\approx }_{\varphi }\mathrm{𝗋𝖺𝗍}(r)$ and $\mathrm{𝗋𝖺𝗍}(r){\sim }_{ϵ-\delta }{y}_{\delta }$, and two unneeded inductive hypotheses.By definition, we have $\eta :{\mathbb{Q}}_{+}$ such that $x_{\eta }{\approx }_{\varphi -\eta }\mathrm{𝗋𝖺𝗍}(r)$, so the inductive triangle inequality gives $x_{\eta }{\approx }_{\varphi +ϵ-\eta -\delta }{y}_{\delta }$.The definition of $\approx$ then immediately yields $\mathrm{𝗅𝗂𝗆}(x){\approx }_{\varphi +ϵ}\mathrm{𝗅𝗂𝗆}(y)$.

3. We assume $\varphi ,ϵ,\delta :{\mathbb{Q}}_{+}$ such that $\mathrm{𝗅𝗂𝗆}(x){\approx }_{\varphi }\mathrm{𝗅𝗂𝗆}(y)$ and $y_{\delta }{\sim }_{ϵ-\delta }\mathrm{𝗋𝖺𝗍}(r)$, and two unneeded inductive hypotheses.By definition we have $\xi ,\theta :{\mathbb{Q}}_{+}$ such that $x_{\xi }{\approx }_{\varphi -\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 }_{\varphi +\delta -\xi }{y}_{\delta }$ and then $x_{\xi }{\sim }_{\varphi +ϵ-\xi }\mathrm{𝗋𝖺𝗍}(r)$.The definition of $\approx$ then gives $\mathrm{𝗅𝗂𝗆}(x){\approx }_{\varphi +ϵ}\mathrm{𝗋𝖺𝗍}(r)$, as desired.

4. Finally, we assume $\varphi ,ϵ,\delta ,\eta :{\mathbb{Q}}_{+}$ such that $\mathrm{𝗅𝗂𝗆}(x){\approx }_{\varphi }\mathrm{𝗅𝗂𝗆}(y)$ and $y_{\delta }{\sim }_{ϵ-\delta -\eta }{z}_{\eta }$.Then as before we have $\xi ,\theta :{\mathbb{Q}}_{+}$ with $x_{\xi }{\approx }_{\varphi -\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 $(\mathrm{𝗋𝖺𝗍}(q){\approx }_{(\text{–})}\text{–})$ and $(\mathrm{𝗅𝗂𝗆}(x){\approx }_{(\text{–})}\text{–})$.Since all are elements of $A$, they are rounded and satisfy the triangle inequality on the right with respect to $\mathrm{\sim }$.What remains is to verify the conditions relating to $⌢$, which is to say that these relations satisfy the triangle inequality on the left with respect to the constructors of $\mathrm{\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 ${ℝ}_{𝖼}$-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\mathrm{,}v\mathrm{:}{\mathrm{R}}_{\mathrm{c}}$ and $ϵ\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}$ we have $\mathrm{(}u{\mathrm{\sim }}_{ϵ}v\mathrm{)}\mathrm{=}\mathrm{(}u{\mathrm{\approx }}_{ϵ}v\mathrm{)}$.

Proof.

Since both are mere propositions, it suffices to prove bidirectional implication.For the left-to-right direction, we use $\mathrm{\sim }$-induction applied to $C(u,v,ϵ):\equiv (u{\approx }_{ϵ}v)$.Thus, it suffices to consider the four constructors of $\mathrm{\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 ${ℝ}_{𝖼}$-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 $\mathrm{\sim }$.∎

Stretching a point, one might call $\approx$ a fibration of “codes” for $\mathrm{\sim }$, with the two directions of the above proof being $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}$ and $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}$ respectively.By the definition of $\approx$, from thm:RC-sim-characterization we get equivalences

$(\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ}\mathrm{𝗋𝖺𝗍}(r))$

$(\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ}\mathrm{𝗅𝗂𝗆}(y))$$=\exists (\delta :{\mathbb{Q}}_{+}).\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ-\delta }{y}_{\delta }$

$(\mathrm{𝗅𝗂𝗆}(x){\sim }_{ϵ}\mathrm{𝗋𝖺𝗍}(r))$$=\exists (\delta :{\mathbb{Q}}_{+}).x_{\delta }{\sim }_{ϵ-\delta }\mathrm{𝗋𝖺𝗍}(r)$

$(\mathrm{𝗅𝗂𝗆}(x){\sim }_{ϵ}\mathrm{𝗅𝗂𝗆}(y))$$=\exists (\delta ,\eta :{\mathbb{Q}}_{+}).x_{\delta }{\sim }_{ϵ-\delta -\eta }{y}_{\eta }.$

Our proof also provides the following additional information.

Corollary 11.3.15.

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

$$(u{\sim }_{ϵ}v)\simeq \exists (\theta :{\mathbb{Q}}_{+}).u{\sim }_{ϵ-\theta }v$$(11.3.15)

$$(u{\sim }_{ϵ}v)\to (v{\sim }_{\delta }w)\to (u{\sim }_{ϵ+\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\mathrm{:}{\mathrm{R}}_{\mathrm{c}}$, Cauchy approximation $y$, and $ϵ\mathrm{,}\delta \mathrm{:}{\mathrm{Q}}_{\mathrm{+}}$, if $u{\mathrm{\sim }}_{ϵ}{y}_{\delta }$ then $u{\mathrm{\sim }}_{ϵ\mathrm{+}\delta }\lim \mathit{}\mathrm{(}y\mathrm{)}$.

Proof.

We use ${ℝ}_{𝖼}$-induction on $u$.If $u$ is $\mathrm{𝗋𝖺𝗍}(q)$, then this is exactly the second constructor of $\mathrm{\sim }$.Now suppose $u$ is $\mathrm{𝗅𝗂𝗆}(x)$, and that each $x_{\eta }$ has the property that for any $y,ϵ,\delta$, if $x_{\eta }{\sim }_{ϵ}{y}_{\delta }$ then $x_{\eta }{\sim }_{ϵ+\delta }\mathrm{𝗅𝗂𝗆}(y)$.In particular, taking $y:\equiv x$ and $\delta :\equiv \eta$ in this assumption, we conclude that $x_{\eta }{\sim }_{\eta +\theta }\mathrm{𝗅𝗂𝗆}(x)$ for any $\eta ,\theta :{\mathbb{Q}}_{+}$.

Now let $y,ϵ,\delta$ be arbitrary and assume $\mathrm{𝗅𝗂𝗆}(x){\sim }_{ϵ}{y}_{\delta }$.By roundedness, there is a $\theta$ such that $\mathrm{𝗅𝗂𝗆}(x){\sim }_{ϵ-\theta }{y}_{\delta }$.Then by the above observation, for any $\eta$ we have $x_{\eta }{\sim }_{\eta +\theta /2}\mathrm{𝗅𝗂𝗆}(x)$, and hence $x_{\eta }{\sim }_{ϵ+\eta -\theta /2}{y}_{\delta }$ by the triangle inequality.Hence, the fourth constructor of $\mathrm{\sim }$ yields $\mathrm{𝗅𝗂𝗆}(x){\sim }_{ϵ+2\eta +\delta -\theta /2}\mathrm{𝗅𝗂𝗆}(y)$.Thus, if we choose $\eta :\equiv \theta /4$, the result follows.∎

Lemma 11.3.17.

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

Proof.

Take $u:\equiv y_{\delta }$ and $ϵ:\equiv \eta$ in the previous lemma.∎

Remark 11.3.18.

We might have expected to have $y_{\delta }{\mathrm{\sim }}_{\delta }\lim \mathit{}\mathrm{(}y\mathrm{)}$, but this fails in examples.For instance, consider $x$ defined by $x_{ϵ}\mathrm{:}\mathrm{\equiv }ϵ$.Its limit is clearly $\mathrm{0}$, but we do not have , only $\mathrm{\le }$.

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

Lemma 11.3.19.

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

$$\forall (u:{ℝ}_{𝖼}).\forall (ϵ:{\mathbb{Q}}_{+}).\exists (\delta :{\mathbb{Q}}_{+}).\forall (v:{ℝ}_{𝖼}).(u{\sim }_{\delta }v)\to (f(u){\sim }_{ϵ}f(v))$$

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

Proof.

We prove $f(u)=g(u)$ for all $u$ by ${ℝ}_{𝖼}$-induction.The rational case is just the hypothesis.Thus, suppose $f(x_{\delta })=g(x_{\delta })$ for all $\delta$.We will show that $f(\mathrm{𝗅𝗂𝗆}(x)){\sim }_{ϵ}g(\mathrm{𝗅𝗂𝗆}(x))$ for all $ϵ$, so that the path constructor of ${ℝ}_{𝖼}$ applies.

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

$(\mathrm{𝗅𝗂𝗆}(x){\sim }_{\theta }v)$$\to (f(\mathrm{𝗅𝗂𝗆}(x)){\sim }_{ϵ/2}f(v))$

$(\mathrm{𝗅𝗂𝗆}(x){\sim }_{\eta }v)$$\to (g(\mathrm{𝗅𝗂𝗆}(x)){\sim }_{ϵ/2}g(v)).$

Choosing , by thm:RC-sim-lim-term we have both $\mathrm{𝗅𝗂𝗆}(x){\sim }_{\theta }{y}_{\delta }$ and $\mathrm{𝗅𝗂𝗆}(x){\sim }_{\eta }{y}_{\delta }$.Hence

$$f(\mathrm{𝗅𝗂𝗆}(x)){\sim }_{ϵ/2}f(y_{\delta })=g(y_{\delta }){\sim }_{ϵ/2}g(\mathrm{𝗅𝗂𝗆}(x))$$

and thus $f(\mathrm{𝗅𝗂𝗆}(x)){\sim }_{ϵ}g(\mathrm{𝗅𝗂𝗆}(x))$ by the triangle inequality.∎