Vaughan Pratt writes:
I would bounce this question back to Martin: what did he mean by "th= e Dedekind reals" in his attribution to Freyd?
I meant (and still mean): the underlying object of the final coalgebra is what topos theorists know as "the object of Dedekind reals" (in an elementary topos with nno). In more detail [Freyd & Johnstone, in Johnstone's Elephant, pages 1028-1032]: given a topos with nno, consider the category of (internal) posets in the topos. In this category, define a functor. Consider its final coalgebra. Theorem: (1) It exists. (2) Moreover, the underlying object of the algebra is the Dedekind unit interval under its natural order. (3) The structure map performs average (x,y) |-> (x+y)/2 (for full details, see the reference). Answering the question quoted below, you get all the ingredients you are looking for: a *set* of numbers (as the underlying set of the underlying poset of the final coalgebra), its *order* (as the underlying object of the final coalgebra), and (part of) its *algebraic* structure (as the structure map of the final coalgebra). Of course, here "set" means an object of a topos, e.g. that of classical sets. You get only part of the *algebraic* structure, but topos logic is strong enough to allow you to fully recov= er=20 it after you have the final coalgebra in your hands.=20 The Escardo-Simpson approach is similar, but takes a different route and makes weaker assumptions - I won't repeat the story, which can be found in the paper whose reference was already given by Alex Simpson. Martin Escardo