From mboxrd@z Thu Jan  1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1382
Path: news.gmane.org!not-for-mail
From: "Martin H. Escardo" <Martin.H.Escardo@ens.fr>
Newsgroups: gmane.science.mathematics.categories
Subject: Re: Freyd's couniversal characterization of [0,1]
Date: Wed, 26 Jan 2000 15:32:49 +0100 (MET)
Message-ID: <200001261432.PAA00407@agaric.ens.fr>
References: <200001241914.UAA23504@agaric.ens.fr>
	<vkaaelt766d.fsf@localhost.localdomain>
NNTP-Posting-Host: main.gmane.org
X-Trace: ger.gmane.org 1241017788 30961 80.91.229.2 (29 Apr 2009 15:09:48 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Wed, 29 Apr 2009 15:09:48 +0000 (UTC)
To: categories@mta.ca
Original-X-From: rrosebru@mta.ca Wed Jan 26 13:18:42 2000 -0400
Original-Received: (from Majordom@localhost)
	by mailserv.mta.ca (8.9.3/8.9.3) id LAA18278
	for categories-list; Wed, 26 Jan 2000 11:31:40 -0400 (AST)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
In-Reply-To: <vkaaelt766d.fsf@localhost.localdomain>
Original-Sender: cat-dist@mta.ca
Precedence: bulk
Original-Lines: 34
Xref: news.gmane.org gmane.science.mathematics.categories:1382
Archived-At: <http://permalink.gmane.org/gmane.science.mathematics.categories/1382>

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