Cartesian bicategories and realizability
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/ ]
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/ ]
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?
You should look at A. Carboni, Some free constructions in realizability and proof theory. J. Pure Appl. Algebra 103 (1995), no. 2, 117–148 J. van Oosten, Realizability: an introduction to its categorical side. Studies in Logic and the Foundations of Mathematics, 152. Elsevier B. V., Amsterdam, 2008 --Pino Rosolini [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Thanks for the helpful replies, everyone. FL Philip Scott wrote:
Dear Finn: as mentioned by Rosolini, you should definitely check out the book of Jaap von Oosten. More interesting from your point of view is to go to Jaap's webpage and look at the rather detailed criticism/ response of Jaap and Johnstone to a review by Peter Johnstone of Jaap's book. That probably has some things you're looking for. And, oc, Johnstone's still working on Elephant Vol.3 (who knows when it will appear) which may have some of this stuff.
There are unpublished notes by P. Freyd (I was at U.Penn on sabbatical in 1987 when he gave a course on this) on realizability topoi based on the allegories/ exact-completion method.
Phil Scott
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (3)
-
Finn Lawler -
flawler＠scss.tcd.ie -
Giuseppe Rosolini