Real midpoints

[Peter Freyd <pjf@saul.cis.upenn.edu>]

It could well be that Vaughan and I are defining the midpoint structure
in the same way. Here's how I described it (using the conventions from
my last posting).

Let  F:I --> I v I  be a final coalgebra. We will denote the top of  I
as  T  and the bottom as  B.  Construct the "halving" map,  h:I --> I,
(on  [-1,1]  it will send  x  to  x/2)  as:  

                   T v F v B             F'v F'        F'
    I --> 1 v I v 1 ------> I v I v I v I ---> I v I  --> I

where  F' denotes the inverse of  F, and, by a little overloading, T
and  B  denote the maps constantly equal to  T  and  B.  The leftmost
map records the fact that the terminator is a unit for the 
ordered-wedge functor.

Let  g  be the endo-function on  I x I  defined recursively by:

    g<x,y> = if  dx = T  and  dy = T  then      <x,y>    else
             if  dx = T  and  uy = B  then  h(g(dx,uy>)  else
             if  ux = B  and  dy = T  then  h(g<ux,dy>)  else
             if  ux = B  and  uy = B  then      <x,y>.

The values of  g  lie in the first and third quadrants, that is, those
points such that either  dx = dy = T  or  ux = uy = B.  The two maps

           g       d x d                   g       u x u
    I x I --> I x I --> I x I  and  I x I --> I x I --> I x I  

give a coalgebra structure on  I x I.  The midpoint operation may be
defined as the induced map to the final coalgebra.