Re: Freyd's couniversal characterization of [0,1]

["Martin H. Escardo" <Martin.H.Escardo@ens.fr>]

Andrej Bauer writes:
 > I can answer this for equilogical spaces.
 > 
 > The functor F: Bi[Equ] ---> Bi[Equ] has a final coalgebra. It
 > is the equilogical space (C, ~) where C is the Cantor space
 > 
 >         C = 2^N = infinite sequences of 0's and 1's
 > 
 > and ~ is the equivalence relation defined by
 > 
 >         a ~ b  iff  r(a) = r(b)
 > 
 > where r: C --> [0,1] is defined by
 > 
 >         r(a) = \sum_{k=0}^\infty a_k / 2^{k+1}

This is interesting in connection with some previous discussion in
this list on "definability" of the mid-point operation "by
coinduction".

As it is well known, the mid-point operation is not continuously
realizable via binary expansions with the Cantor topology. 

(As Andrej Bauer and other people have mentioned signed-digit binary
expansions in this discussion, let me emphasize that, in contrast to
the above situation, all continuous functions [-1,1]^n->[-1,1] are
continuously realizable via signed-digit binary expansions with the
Cantor topology. Put in another way, the space 3^N = (3^N)^n is
projective over (the regular epimorphism) s:3^N->[-1,1], but the space
2^N is not projective over r:2^N->[0,1].)

Martin Escardo