From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6418 Path: news.gmane.org!not-for-mail From: flawler@scss.tcd.ie Newsgroups: gmane.science.mathematics.categories Subject: Re: Cartesian bicategories and realizability Date: Sun, 12 Dec 2010 14:11:56 -0000 (GMT) Message-ID: Reply-To: flawler@scss.tcd.ie NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1292242860 23416 80.91.229.12 (13 Dec 2010 12:21:00 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Mon, 13 Dec 2010 12:21:00 +0000 (UTC) Cc: categories@mta.ca To: "James Lipton" Original-X-From: majordomo@mlist.mta.ca Mon Dec 13 13:20:55 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.114]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1PS7Oh-0001G5-E6 for gsmc-categories@m.gmane.org; Mon, 13 Dec 2010 13:20:55 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:45596) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1PS7OG-0004pS-IS; Mon, 13 Dec 2010 08:20:28 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1PS7OD-0004Wn-Ek for categories-list@mlist.mta.ca; Mon, 13 Dec 2010 08:20:25 -0400 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6418 Archived-At: James Lipton wrote: > This sounds a bit like the construction of realizability toposes in > Categories and Allegories (Freyd and Scedrov) Thanks. I don't have access to that book at the moment, but I seem to remember that they don't mention triposes. Do you know if anyone has studied realizability triposes by looking at their associated allegories/bicategories of relations, and/or compared (in that context or another) the category-of-pers construction of realizability toposes with the exact-completion method? FL > Best, > Jim Lipton > > On Fri, Dec 10, 2010 at 12:12 PM, wrote: > >> Hello all, >> >> I've been trying to understand the different constructions of >> realizability toposes, namely the category of pers in a tripos and the >> exact completion of a category of partitioned assemblies, and how they >> are >> related. >> >> I think that the category-of-pers construction can be recast as follow= s: >> considering a tripos as a monoidal fibration, take the corresponding >> bicategory of relations (as in e.g. [1]), split the symmetric >> idempotents, >> and take the bicategory of maps, which turns out to be equivalent to a >> 1-category that in fact is a topos. >> >> This can be done in two stages, by splitting first the coreflexives an= d >> then the equivalence relations. The result of the first step (at leas= t >> in >> the case of the effective tripos) is the category of assemblies. The >> latter is also the regular completion of the category of partitioned >> assemblies. >> >> If this is right, then the effective topos is the category of maps in >> the >> symmetric-idempotent splitting of two (non-equivalent) bicategories: t= he >> bicategory arising from the effective tripos, and the (local preorder >> reflection of the) bicategory of spans of partitioned assemblies. >> >> I would like to be able to express all of this, and to compare the two >> kinds of construction further, in the language of cartesian >> bicategories, >> which seems like the natural context (especially if one doesn't want t= o >> assume that everything is locally preordered). The closest thing in t= he >> literature that I'm aware of is [2], but that paper predates a lot of >> recent results on cartesian bicategories and on realizability. >> >> So my questions are these: does this make sense, or have I made some >> kind >> of silly mistake? Has there been any work on understanding and >> comparing >> the usual realizability constructions in this sort of context? >> >> Thanks for your attention so far, and thanks in advance for any replie= s. >> >> >> Finn Lawler >> >> >> References: >> >> [1] Mike Shulman, `Framed bicategories and monoidal fibrations', TAC >> 20(18), 2008 >> >> [2] Du=C5=A1ko Pavlovic, `Maps II: Chasing diagrams in categorical pro= of >> theory', Logic Journal of the IGPL, 4(2), 1996 >> >> >> >> >> [For admin and other information see: >> http://www.mta.ca/~cat-dist/] >> > -- Finn Lawler [For admin and other information see: http://www.mta.ca/~cat-dist/ ]