From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2131 Path: news.gmane.org!not-for-mail From: Martin Escardo Newsgroups: gmane.science.mathematics.categories Subject: Re: What does it take to identify the field and the continuum of reals? Date: Mon, 27 Jan 2003 11:50:27 +0000 Message-ID: <15925.7427.766854.416003@acws-0054.cs.bham.ac.uk> References: <200301252120.NAA26529@coraki.Stanford.EDU> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII X-Trace: ger.gmane.org 1241018433 2631 80.91.229.2 (29 Apr 2009 15:20:33 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:20:33 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Mon Jan 27 12:33:44 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 27 Jan 2003 12:33:44 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18dC91-0000pw-00 for categories-list@mta.ca; Mon, 27 Jan 2003 12:29:59 -0400 In-Reply-To: <200301252120.NAA26529@coraki.Stanford.EDU> X-Mailer: VM 6.89 under 21.1 (patch 14) "Cuyahoga Valley" XEmacs Lucid Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 56 Original-Lines: 37 Xref: news.gmane.org gmane.science.mathematics.categories:2131 Archived-At: Vaughan Pratt writes: > I would bounce this question back to Martin: what did he mean by "th= e > Dedekind reals" in his attribution to Freyd? I meant (and still mean): the underlying object of the final coalgebra is what topos theorists know as "the object of Dedekind reals" (in an elementary topos with nno). In more detail [Freyd & Johnstone, in Johnstone's Elephant, pages 1028-1032]: given a topos with nno, consider the category of (internal) posets in the topos. In this category, define a functor. Consider its final coalgebra. Theorem: (1) It exists. (2) Moreover, the underlying object of the algebra is the Dedekind unit interval under its natural order. (3) The structure map performs average (x,y) |-> (x+y)/2 (for full details, see the reference). Answering the question quoted below, you get all the ingredients you are looking for: a *set* of numbers (as the underlying set of the underlying poset of the final coalgebra), its *order* (as the underlying object of the final coalgebra), and (part of) its *algebraic* structure (as the structure map of the final coalgebra). Of course, here "set" means an object of a topos, e.g. that of classical sets. You get only part of the *algebraic* structure, but topos logic is strong enough to allow you to fully recov= er=20 it after you have the final coalgebra in your hands.=20 The Escardo-Simpson approach is similar, but takes a different route and makes weaker assumptions - I won't repeat the story, which can be found in the paper whose reference was already given by Alex Simpson. Martin Escardo