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