25 Jan
2003
25 Jan
'03
2:21 a.m.
Set. Do you think your construction works in any topos?
the coalgebraic structures are defined using just arithmetic. in the first one, there is the "no infinite sequences of 1s" condition, which i am reminded depends on markov's principle; but that is just used in the explanation. i don't think there are other constraints.
If so, what would "Cauchy reals" mean precisely in this general context?
it means fundamental sequence, with the equivalence relation in the "lazy" mode, a la bishop, as described in andrej bauer's message. if my last night's posting makes sense, then these constructivist cauchy reals make a whole lot of difference, because they really let you avoid the choice and get limits. -- dusko