Re: Cartesian bicategories and realizability

Re: Cartesian bicategories and realizability

[flawler]

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

Re: Cartesian bicategories and realizability

[Giuseppe Rosolini]

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

Re: Cartesian bicategories and realizability

[Finn Lawler]

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

Cartesian bicategories and realizability

[flawler]

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