Category Theory
Zulip Server
Archive

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.

Stream: theory: category theory

Topic: Kripke CPS and Sheaves

Dan Doel (Apr 20 2020 at 03:03):

@Cody Roux By the way, a while back someone told me you wanted to know the connection between Continuation-passing Style Models Complete for Intuitionistic Logic and sheaves. I was going to write something explaining what I understood of it, but then I got sidetracked, and maybe this is a better place to answer anyway, because other people can fill in blanks I don't really understand.

So, the bit I can explain is just kind of based in general category stuff, with only a little information on sheaves. What the paper seems to be doing breaks down to this:

1. There is an ordinary Kripke/sheaf style thing where you interpret logical operations into presheaves.
2. There is an 'exploding' relation between worlds and formulae. I think this is given by the model, and it's only used in one way in the paper, as I recall. But in general I think it gives you the 'topology' for the model. However, it seems like the way it does that is by just giving a sheaf interpretation of every formula. Perhaps it's not that simple, because maybe you're not obliged to give something that actually behaves correctly; I'm not sure. In the paper, this is just the yoneda embedding.
3. You take part 1 and you "CPS" it by part 2. In the paper, this looks like $\int_C [[KA,EC],EC]$ where you're interpreting formula $A$, $K$ is the Kripke interpretation of the formula, and $E$ is the 'exploding' interpretation of a formula. I think this is unnecessarily complicated, though, because it uses the internal hom twice instead of powers and the external hom.

In the paper, it actually ends up using contexts as 'worlds', too, which is why it can use the yoneda embedding as $E$. So, it's interpreting the logic into presheaves on the context category, and then doing the CPS thing with representable presheaves. But if you look at that limit, It's basically the formula for $Ran U 1$, where $U$ is the inclusion of representables into all presheaves. But that is equivalent to the left adjoint of $U$ if it exists, and as long as $E$ can be thought of as a subcategory of sheaves, then the left adjoint to $U$ is sheafification.

Maybe this still works out even when $E$ isn't exactly a category of sheaves, and gives you the sheaves that would occur by interpreting. $E$ as some kind of topology. I'm not sure. I'm also not sure if there's a topology for exactly the representable functors. Those would be the sort of questions that perhaps someone more knowledgeable could fill in.

Dan Doel (Apr 20 2020 at 03:20):

Oh, also, it's possible that the double internal hom looking thing is also part of fixing things up if $E$ is not properly functorial or something. I'm not certain.

Cody Roux (Apr 20 2020 at 12:09):

Thanks so much @Dan Doel! I need to chew on this a bit. I'd also like to start a stream on NbE, but I'm not sure I have the energy to drive it right now.