I am deeply embarrassed at not drawing this inference myself. I noticed the felicitous identification of 0111... and 1000... but the importance of the resulting redundancy didn't click. That the whole process happened in one step led me to think that the representation was as irredundant as all extant one-step constructions. The fact that addition is easier to define with Peter's functor than with ours should have been a big hint.
Well, maybe not so embarrassed after all. Although there is some redundancy, as Peter Selinger pointed out to me (in the same message where he pointed out the problem with 1->3) there isn't enough redundancy to make the function constituting Peter F.'s midpoint coalgebra computable, at least not corecursively. Given say -++---+-++... and +--+++-+--... (two complementary reals x and -x, which must therefore sum to zero), if they stay complementary forever one can output either of +---------... or -+++++++++... forever, with one output bit per input bit. These two infinite sequences redundantly represent zero (as does the empty sequence). Furthermore if one pictures oneself as outputting both infinite sequences (justified by the idea that in the limit they become the same real), then one can discard the "wrong" one when it is discovered that the two inputs aren't complementary. Addition defined corecursively in this way is effective. But while this is computationally appealing, technically speaking it isn't quite coinduction, which makes no provision for hedging one's bets by carrying along both possibilities when you can't make up your mind. To make traditional redundant computer arithmetic work coinductively, more redundancy is needed. To that end I tried tripointed sets, calling the constants -,0,+, along with a functor 3(X) that makes not two but three copies of X and pastes their constants together as follows: - 0 + - 0 + - 0 + ------------- - . 0 . + The idea is that the constants denote -1, 0, and 1 respectively and that 3(I) somehow is isomorphic to I, with the two dots becoming -1/2 and 1/2 respectively. But for that to work 3(-) would have to paste a lot more points than it does. So this seems like a nice question: is there a category C and a functor F:C->C whose final coalgebra is the continuum with sufficiently redundant coalgebraic structure to permit addition to be defined coinductively? Vaughan