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