On Wed, 11 Feb 2009, Vaughan Pratt wrote:
Prof. Peter Johnstone wrote:
Whoa! This simply can't work. Whatever the final coalgebra for N x (-) looks like, it must (thanks to Lambek) be isomorphic to N x itself, and therefore (since equality for N is decidable) must have lots of complemented subobjects {0} x itself, {1} x itself, ... The point of the continuity theorem for functions R --> R is that there are toposes in which R has *no* nontrivial complemented subobjects [...] The only way to get round it (apart from using glue) is to replace N by some "nonstandard natural number object" having no nontrivial complemented subobjects -- but where you get that from, I don't know.
You're assuming product distributes over sums, which would be true for ordinary product but I specified lexicographic product, with the left argument as the "high order digit" (converse of the usual convention for ordinal product in ordinal arithmetic).
For goodness' sake, Vaughan! How many times do I have to tell you that I'm talking about *the underlying object* of the final coalgebra, and not its order structure or its topology? If the underlying object of the lexicographic product is the ordinary (cartesian) product -- and if it's not, then I don't know what it is -- then it distributes over sums because that's what products do in a topos.
Why should {0} x N be a complemented subobject of N x N when lexicographic product attaches the "end" of it to {1} x {0} , which I would expect it will in a topos of sheaves when participating in a final coalgebra for N x X.
The order structure can't do any sort of "attaching" that negates the complementedness of the underlying subobject, and neither can the topology. The only thing that can do that is to make identifications between endpoints -- i.e. to use "glue" a la Freyd. Peter