From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7459 Path: news.gmane.org!not-for-mail From: Jonas Frey Newsgroups: gmane.science.mathematics.categories Subject: Re: An internal definition in a realizability topos Date: Wed, 26 Sep 2012 19:58:43 +0200 Message-ID: References: Reply-To: Jonas Frey NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: ger.gmane.org 1348685182 25198 80.91.229.3 (26 Sep 2012 18:46:22 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 26 Sep 2012 18:46:22 +0000 (UTC) Cc: categories list To: Andrej Bauer Original-X-From: majordomo@mlist.mta.ca Wed Sep 26 20:46:25 2012 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.134]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1TGwcm-0003af-NR for gsmc-categories@m.gmane.org; Wed, 26 Sep 2012 20:46:20 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:54934) by smtpx.mta.ca with esmtp (Exim 4.77) (envelope-from ) id 1TGwc2-0007SC-Qn; Wed, 26 Sep 2012 15:45:34 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1TGwc6-000054-1r for categories-list@mlist.mta.ca; Wed, 26 Sep 2012 15:45:38 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7459 Archived-At: Dear Andrej, the object that you are interested in has been studied by Jaap van Oosten in his preprint "A Notion of Homotopy for the Effective Topos" www.staff.science.uu.nl/~ooste110/realizability/homtpyEff.pdf A way to define it abstractly -- not using concepts that are particular to realizability -- is as a "gluing of intervals Nabla(2)", more precisely as the colimit of the diagram Nabla(2) <- 1 -> Nabla(2) <- 1 -> Nabla(2) <- ... <- 1 -> Nabla(2). I don't know if this counts as a "definition in the internal language" for you, but certainly the universal property can be expressed in the internal language, i.e. there is a judgment about cocones which holds iff the cocone is a colimit cocone. Kind regards, Jonas On Mon, Sep 24, 2012 at 5:52 PM, Andrej Bauer wrote: > Consider a realizability topos RT(A) over some PCA A. There is an > embedding Nabla : Set -> RT(A), which takes a set X to the assembly > whose underlying set is X and the existence predicate is trivial, > i.e., every element of X is realized by every realizer of A. > > Let [n] = {0, 1, 2, .., n-1} be the set with n elements. I have some > interest in the subobject of Nabla([n]) whose underlying set is [n] > and the existence predicate is > > E(0) = { numeral(0) } > E(1) = { numeral(0), numeral(1) } > ... > E(k) = { numeral(k-1), numeral(k) } > ... > E(n-1) = {numeral(n-2)} > > In words: there are n elements 0, 1, 2, ..., n-1, where two > consequtive elements share a realizer. > > The question is; is this object definable in the internal language of the topos? > > Note that Nabla(2) is definable as the object of not-not-stable truth > values, and that each Nabla(X) is also definable with a bit more work. > > With kind regards, > > Andrej > > > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] [For admin and other information see: http://www.mta.ca/~cat-dist/ ]