arithmetical and geometric reals in (models of) SDG

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

Recently I was asking myself what is the relation between the arithmetical
(Dedekind) reals in a topos and a ring R satisfying the usual SDG axioms
(i.e. at least the Kock-Lawvere) axiom.

>From the few things I know about models of SDG it seems to me as if in the
usual sheaf models (over a site Loc of `loci') the Dedekind reals form a
subring of R = y(\Re) (where \Re is the locus corresponding to the reals).
As long as one considers just presheaves that's clear as the Dedekind reals
are given by \Delta(\Re).
Probably taking sheaves that situation isn't changed dramatically?

So my impression is that in the usual sheaf models of SDG the real line R
carries the structure of an algebra over the Dedekind reals. However, I don't
see how to construct such an embedding of Dedekind reals into R based only
on the usual axioms of SDG. Of course, when given an order on R and R is
assumed as a Q-algebra then one has a good candidate for a function from R
to R_D sending x \in R to {q \in Q | q.1 \leq x}. But how to define purely
logically an embedding of R_D into R remains mysterious (to me).

I am fully aware of the fact that my question is a bit `against the strain'
of SDG but we know that both kinds of reals do coexist in topos models.
But is this coexistence only peaceful or rather more collaborative?

I am certain that people must have thought about this but I couldn't find
anything at the usual places where to look. So I would be grateful for
comments (on the correctness of my above speculations) or pointers to
existing literature or folklore.

Best, Thomas Streicher