Vaughan Pratt wrote in part:
Prof. Peter Johnstone wrote:
How do you (constructively) give N^N the order type of the nonnegative reals?
One way to see this is to replace the 0's in the usual binary expansion of x \in [0,1) by commas and read the resulting comma-separated blocks of 1's as tally notation.
But it's not a constructive theorem that every such x has a binary expansion. That's still a neat result, that the binary reals are given by N^N, but the binary reals aren't constructively the same as the reals.
is there a topos in which the order type of the Freyd coalgebra is not that of the (forward) lexicographic ordering of N^N (modulo endpoints)?
In the topos of sheaves on the real line, every function from [0,1) to N is constant, yet there are obviously many other functions from N^N to N. Thus N^N and [0,1) are not constructively isomorphic as sets, so there is no way to give N^N the order type of [0,1) constructively. --Toby