From mboxrd@z Thu Jan 1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/40
Path: news.gmane.org!not-for-mail
From: "Prof. Peter Johnstone"
Newsgroups: gmane.science.mathematics.categories
Subject: Re: "Kantor dust"
Date: Tue, 3 Feb 2009 17:59:58 +0000 (GMT)
Message-ID:
Reply-To: "Prof. Peter Johnstone"
NNTP-Posting-Host: lo.gmane.org
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
X-Trace: ger.gmane.org 1233708473 21389 80.91.229.12 (4 Feb 2009 00:47:53 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Wed, 4 Feb 2009 00:47:53 +0000 (UTC)
To: Vaughan Pratt , categories list
Original-X-From: categories@mta.ca Wed Feb 04 01:49:07 2009
Return-path:
Envelope-to: gsmc-categories@m.gmane.org
Original-Received: from mailserv.mta.ca ([138.73.1.1])
by lo.gmane.org with esmtp (Exim 4.50)
id 1LUVww-0005zD-95
for gsmc-categories@m.gmane.org; Wed, 04 Feb 2009 01:49:06 +0100
Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1LUVKt-0000tQ-SP
for categories-list@mta.ca; Tue, 03 Feb 2009 20:09:47 -0400
Original-Sender: categories@mta.ca
Precedence: bulk
Xref: news.gmane.org gmane.science.mathematics.categories:40
Archived-At:
On Mon, 2 Feb 2009, Vaughan Pratt wrote:
> How about the converse: does N entail K? In any topos with NNO N the
> underlying object of the final coalgebra of FX = X+X is presumably 2^N.
> Does the Elephant prove that 2^N can be made a final coalgebra of X+X?
>
It's not in the Elephant; but it's an easy exercise in primitive
recursion, given a coalgebra structure X \to X + X, to define the
transpose N x X \to 2 of the unique coalgebra morphism X \to 2^N.
> And if so, what other coalgebras are brought into existence by N? For
> example can N^N be made a doubly inductive (inductive-coinductive)
> coalgebra encoding the lexicographic order that gives N^N the order type
> of the nonnegative reals? That would give a pretty direct construction
> of the usual topology of the real line in any topos with NNO. (This is
> the one-dimensional conception of the continuum, as opposed to the
> zero-dimensional conception preferred by descriptive set theorists, who
> take the continuum to be N^N with the ordinary product topology.)
>
How do you (constructively) give N^N the order type of the nonnegative
reals? I know how to give it the order type of the irrationals, but
that's still zero-dimensional. However, Freyd's presentation of the
real unit interval as a final coalgebra is done constructively (for any
topos with NNO) in the Elephant, D4.7.17.
Peter Johnstone