Re: "Kantor dust"

["Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>]

On Mon, 2 Feb 2009, Vaughan Pratt wrote:

> How about the converse: does N entail K?  In any topos with NNO N the
> underlying object of the final coalgebra of FX = X+X is presumably 2^N.
>  Does the Elephant prove that 2^N can be made a final coalgebra of X+X?
>
It's not in the Elephant; but it's an easy exercise in primitive
recursion, given a coalgebra structure X \to X + X, to define the
transpose N x X \to 2 of the unique coalgebra morphism X \to 2^N.

> And if so, what other coalgebras are brought into existence by N?  For
> example can N^N be made a doubly inductive (inductive-coinductive)
> coalgebra encoding the lexicographic order that gives N^N the order type
> of the nonnegative reals?  That would give a pretty direct construction
> of the usual topology of the real line in any topos with NNO.  (This is
> the one-dimensional conception of the continuum, as opposed to the
> zero-dimensional conception preferred by descriptive set theorists, who
> take the continuum to be N^N with the ordinary product topology.)
>
How do you (constructively) give N^N the order type of the nonnegative
reals? I know how to give it the order type of the irrationals, but
that's still zero-dimensional. However, Freyd's presentation of the
real unit interval as a final coalgebra is done constructively (for any
topos with NNO) in the Elephant, D4.7.17.

Peter Johnstone