From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6417 Path: news.gmane.org!not-for-mail From: flawler@scss.tcd.ie Newsgroups: gmane.science.mathematics.categories Subject: Cartesian bicategories and realizability Date: Fri, 10 Dec 2010 17:12:12 -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 1292070816 9623 80.91.229.12 (11 Dec 2010 12:33:36 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Sat, 11 Dec 2010 12:33:36 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Sat Dec 11 13:33:32 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 1PROdn-0001ps-Sh for gsmc-categories@m.gmane.org; Sat, 11 Dec 2010 13:33:32 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:54243) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1PROdI-00089L-Kj; Sat, 11 Dec 2010 08:33:00 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1PROdE-0001PT-KW for categories-list@mlist.mta.ca; Sat, 11 Dec 2010 08:32:56 -0400 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6417 Archived-At: 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 ar= e related. I think that the category-of-pers construction can be recast as follows: 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 and then the equivalence relations. The result of the first step (at least i= n 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: the 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 to assume that everything is locally preordered). The closest thing in the 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 replies. Finn Lawler References: [1] Mike Shulman, `Framed bicategories and monoidal fibrations', TAC 20(18), 2008 [2] Du=9Ako Pavlovic, `Maps II: Chasing diagrams in categorical proof theory', Logic Journal of the IGPL, 4(2), 1996 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]