Re: Cauchy completeness of Cauchy reals

["Mamuka Jibladze" <jib@rmi.acnet.ge>]

> NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex
> Simpson and I characterized "the Cauchy completion of the rationals
> within the Dedekind reals" as a free algebra (to be precise, we
> started from the algebras as a primitive notion and later found this
> construction of the free one). But this has already been discussed in
> postings in the past few years.
>
> Martin Escardo

Does one get any known versions of reals by performing the Cauchy or
Dedekind construction starting with initial algebras I for non-decidable
lifts L
instead of the NNO? It would be then also natural to interpret Cauchy
sequences and completeness using appropriate I-indexed families, of course.

Even for "integers" Z one has at least three different options:
taking I^op+1+I, taking the colimit of I->LI->LLI->..., each map being
the unit, or taking the colimit of the corresponding I-indexed diagram.
It would be strange if these turn out to be isomorphic. Is any of them an
initial
algebra for some simple functor?

Similarly there are various possibilities for rationals - taking fractions,
i.e. a quotient
of ZxZ, or colimit of all multiplication maps Z->Z, or of the corresponding
Z-indexed
diagram.

Actually I have not followed the ongoing research for a while, so maybe my
questions
are outdated. I would be grateful for any references to related work.

Mamuka Jibladze