# Chapter 11 Notes

Our treatment of the Dedekind reals borrows many ideas from [BauerTaylor09] where the Dedekind reals are constructed in the context of Abstract Stone Duality. This is a (restricted) form of simply typed $\lambda$-calculus with a distinguished object $\Sigma$ which classifies open sets, and by duality also the closed ones. In [BauerTaylor09] you can also find detailed proofs of the basic properties of arithmetical operations  .

The fact that $\mathbb{R}_{\mathsf{c}}$ is the least Cauchy complete     archimedean  ordered field, as was proved in \autorefRC-initial-Cauchy-complete, indicates that our Cauchy reals probably coincide with the Escardó-Simpson reals [EscardoSimpson:01]. It would be interesting to check whether this is really the case. The notion of Escardó-Simpson reals, or more precisely the corresponding closed interval   , is interesting because it can be stated in any category with finite products  .

In constructive set theory augmented by the “regular extension axiom”, one may also try to define Cauchy completion by closing under limits of Cauchy sequences   with a transfinite iteration. It would also be interesting to check whether this construction agrees with ours.

It is constructive folklore that coincidence of Cauchy and Dedekind reals requires dependent choice but it is less well known that countable choice suffices. Recall that dependent choice states that for a total relation $R$ on $A$, by which we mean $\forall(x:A).\,\exists(y:A).\,R(x,y)$, and for any $a:A$ there merely exists $f:\mathbb{N}\to A$ such that $f(0)=a$ and $R(f(n),f(n+1))$ for all $n:\mathbb{N}$. Our \autorefwhen-reals-coincide uses the typical trick for converting an application of dependent choice to one using countable choice. Namely, we use countable choice once to make in advance all the choices that could come up, and then use the choice function to avoid the dependent choices.

The intricate relationship between various notions of compactness in a constructive setting is discussed in [bridges2002compactness]. Palmgren [Palmgren:FT] has a good comparison between pointwise analysis  and pointfree topology.

The surreal numbers were defined by [conway:onag], using a sort of inductive definition but without justifying it explicitly in terms of any foundational system. For this reason, some later authors have tended to use sign-expansions or other more explicit presentations which can be coded more obviously into set theory  . The idea of representing them in type theory  was first considered by Hancock, while Setzer and Forsberg [forsbergfinite] noted that the surreals and their inequality relations $<$ and $\leq$ naturally form an inductive-inductive definition. The higher inductive-inductive version presented here, which builds in the correct notion of equality for surreals, is new.

Title Chapter 11 Notes
\metatable