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