You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Liang-Ting Chen (Nov 12 2020 at 06:57):Hi, I wonder where I can find references on realizability topos for partial combinatory algebra within other ambient topos rather than Set. It will be nice if this can be constructed via assemblies or PER. It is noted in the nLab (https://ncatlab.org/nlab/show/realizability+topos) that it is not a problem at all, but I fail to find any reference for it.
Matteo Capucci (he/him) (Nov 12 2020 at 08:41):I think Van Oosten's Categorical Realizability covers relative realizability
Matteo Capucci (he/him) (Nov 12 2020 at 08:41):But maybe that's not what you're after
Matteo Capucci (he/him) (Nov 12 2020 at 08:43):The fact that something can be done in a topos depends only on the logic power needed to do that something, and topoi accomodate quite a lot of power. This is to say that it's easy to say 'X can be done in any topos' without actually doing so. Hence it may very well be the case that who wrote that on the nlab just noticed PCAs and their relative realizability topoi can be, in principle, constructed in every topos, without having done so themselves
Matteo Capucci (he/him) (Nov 12 2020 at 08:44):Maybe a more general query like 'internal topos theory' might give you some surface of attack
Liang-Ting Chen (Nov 12 2020 at 08:55):Aha, thanks for the keyword. Indeed, it is not hard to define PCAs internally and I image that defining the category of assemblies internally shouldn't be a problem at all. After all, I have formalised part of developments in Agda which can be interpreted in any model of it. I just kind of feel that there must be written somewhere so that I don't have to invent the wheel again.
Chad Nester (Nov 12 2020 at 09:29):I don’t know if it will help you but my MSc thesis is about something similar. In it I construct a category of “assemblies” for a Cartesian restriction functor, with the domain acting as a category of realisers, and the codomain acting like the ambient logical theory (being in the extreme case a partial topos). From this category of “assemblies” one can recover a topos by methods that rhyme with the usual ones, given enough structure in the domain and codomain of the aforementioned functor. The scare quotes are because I made a silly error and the “assemblies” would be better called “proto-assemblies”, since they do not carry the requirement that every element of the carrier be associated with at least one realizer. I still haven’t gotten around to writing a readable version of any of this, but if you’re interested you can find it here: https://www.ioc.ee/~cneste/files/msc-thesis.pdf
Chad Nester (Nov 12 2020 at 09:37):I’ll mention that if the codomain of this functor is in fact a partial topos you have enough internal logic to define assemblies that do satisfy the missing requirement.
Liang-Ting Chen (Nov 12 2020 at 09:43):@Chad Nester That's very helpful!!! I will have a look and see how much I actually need.
Morgan Rogers (he/him) (Nov 12 2020 at 09:44):Where "partial topos" means quasi-topos? or pretopos? or -pretopos? or one of the Benabou-Streicher notions of partial topos in the paper that comes up when I search that term?
Chad Nester (Nov 12 2020 at 10:03):In the restriction-categorical jargon a partial topos is a discrete cartesian closed restriction category in which every partial monic has a partial inverse. If you leave off that last bit about partial monics then I'm pretty sure you get a "partial quasitopos", although afaik this isn't nailed down anywhere.
Chad Nester (Nov 12 2020 at 10:04):Less imposingly, a partial topos is (more or less) the partial map category of a topos. This was originally worked out in: https://core.ac.uk/download/pdf/81167908.pdf
Morgan Rogers (he/him) (Nov 12 2020 at 10:24):Thanks! I appreciate the reference.
Tom de Jong (Nov 13 2020 at 11:11):Liang-Ting Chen said:
Hi, I wonder where I can find references on realizability topos for partial combinatory algebra within other ambient topos rather than Set. It will be nice if this can be constructed via assemblies or PER. It is noted in the nLab (https://ncatlab.org/nlab/show/realizability+topos) that it is not a problem at all, but I fail to find any reference for it.
You might be interested in Wouter Stekelenburg's PhD thesis "Realizability Categories" (https://dspace.library.uu.nl/handle/1874/260492).
From that thesis (Introduction of Chapter 1):
We develop realizability internally in arbitrary Heyting categories. This class of categories includes all toposes, but also categories that do not have powerobjects.
Also, "relative realizability" is different from "internal realizability". From Section 4.5 of Jaap van Oosten's "Realizability: An Introduction to its Categorical Side"):
'Relative realizability' [refers to] a number of realizability interpretations which arise from an elementary inclusion of pca's.
Matteo Capucci (he/him) (Nov 13 2020 at 11:45):Tom de Jong said:
Also, "relative realizability" is different from "internal realizability". From Section 4.5 of Jaap van Oosten's "Realizability: An Introduction to its Categorical Side"):
'Relative realizability' [refers to] a number of realizability interpretations which arise from an elementary inclusion of pca's.
Yes, I initially misread the question, hope it didn't confuse anyone!
Liang-Ting Chen (Nov 14 2020 at 05:35):Tom de Jong said:
You might be interested in Wouter Stekelenburg's PhD thesis "Realizability Categories" (https://dspace.library.uu.nl/handle/1874/260492).
Thanks! This is exactly what I was looking for. I am also lately aware of Birkedal and van Oosten's paper (https://www.sciencedirect.com/science/article/pii/S0168007201001221) which begins with internal PCA in an arbitrary topos.