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] Duko 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/ ]