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