Categorical semantics for S5 modal logic?

Does anyone know where I can look to find out what the generally categorical semantics of S5 is?

For S4, the answer is well-known: we want a Cartesian closed category with a product-preserving comonad to model $\Box$ and a monad strong with respect to the comonad to model $\Diamond$.

In Awodey's book on category theory, on page 235 he remarks in passing that this setup becomes S5 when the monad is left adjoint to the comonad. However, he doesn't give a reference.

• Now you've peeked my curiosity: what is the point of having such a categorical semantics? Whenever I used S5 it felt like cutting corners. Its properties are really convenient but the implications of logical omniscience were hardly justifiable in the context of systems constrained by computational reality. – Kai Feb 19 '17 at 9:00
• @Kai: I have worked out a natural deduction calculus for what I believe is S5. Since a categorical semantics gives a semantics for proofs, it's very convenient for checking whether this calculus can be interpreted the way I want it to. (For example, I want to make sure normalization is semantics-preserving.) The reason I'm interested in this is that the standard (McCain/Turner/Pearl) accounts of causal inference model causal entailment as $A \to \Box B$, and I'm curious if this can lead to any abstractions for imperative programming which differ from the common monadic abstractions. – Neel Krishnaswami Feb 19 '17 at 20:50
• This situation has only degenerate set-theoretic models. I don't know if that's a bug or feature. Specificially, if $\Diamond \dashv \square$ are an adjoint pair of monad $\Diamond$ and a comonad $\square$ over $\mathbf{Set}$, then the following argument shows $\Diamond \cong - \times A$ and $\square \cong (-)^A$: Choose (of course) $A := \Diamond 1$ and calculate: $\Diamond X \cong \Diamond \sum_{x \in X} 1 \cong \sum_{x \in X} \Diamond 1 = \sum_{x \in X} A \cong X\times A$. You can probably repeat a similar argument when the category is sufficiently concrete and well-behaved. – Ohad Kammar Feb 21 '17 at 22:26
• @OhadKammar: Now I think Awodey's semantics can't be right: if $\Diamond$ is left adjoint to $\Box$, then $\Box \Diamond A \to A$. I guess my question is still a question! – Neel Krishnaswami Feb 22 '17 at 9:53
• I don't understand how you inferred that. Don't you mean $A \rightarrow \square\Diamond A$? – Ohad Kammar Feb 22 '17 at 13:56