Re: "Kantor dust"

[Vaughan Pratt <pratt@cs.stanford.edu>]

Prof. Peter Johnstone wrote:
> A topos with a Cantor set object (i.e. a final coalgebra for FX = X+X)
> necessarily has a natural number object. Observe that the Cantor set K
> necessarily has a point (since 1 has an F-coalgebra structure), so the
> isomorphism K+K \cong K yields a monomorphism K \to K and a point
> disjoint from its image. From there on, use Corollary D5.1.3 in the
> Elephant.

Oh, of course: pick a point out of one half and recurse on the other.
Very plausible that that would work in any topos, but it's great to be
able to stare at an actual proof.  Thank you!

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?

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.)

Does \Omega^N as the final coalgebra for FX = \Omega x X ever arise in
practical situations where \Omega is more than just a pointed version of
1+1 as in Set, e.g. graph theory?

Vaughan Pratt