categories: Re: squares and cubes

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

>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