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, <flawler@scss.tcd.ie> 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 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 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: 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ško 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/<http://www.mta.ca/%7Ecat-dist/>]
-- Finn Lawler [For admin and other information see: http://www.mta.ca/~cat-dist/ ]