Cartesian bicategories and realizability

[flawler@scss.tcd.ie]

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