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: learning: questions

Topic: Double negation fibrewise and another modality "on the base"

David Michael Roberts (Aug 14 2023 at 03:40):

I'm thinking a bit about modal logic in a more constructive context at the moment, particularly in a setting something like dependent type theory (which I try to think of via categorical semantics). I've got Alex Simpson's thesis open, and I've seen @Valeria de Paiva's article "Basic Constructive Modality" with Ritter, where they discussion both the variant IK in Simpson's thesis (also independently discussed by others) and the variant CK.

What I was thinking of trying to understand was a simple example in dependent type theory where one has a dependent type/display map in semantics, and what it looks like to have a modality like necessity that operates on the base type/codomain object, and then on each "fibre" have a double negation. I have only the vaguest of ideas, so if anyone can tell what it might be that I'm grasping for, I'd be grateful for some pointers.

David Michael Roberts (Aug 14 2023 at 03:42):

I also am aware of David Corfield's book on modal homotopy type theory. It might be what I want is in there, but while I read through a chunk of it a couple of years ago, I don't recall offhand anything like what I'm thinking of.

David Michael Roberts (Aug 14 2023 at 03:45):

From a category-theoretic perspective, maybe I want to think of an internal presheaf on some object of a base category, equipped with some modality operator, but taking values in some other internal category that is equipped with a $\neg\neg$ operator. The "other internal category" is probably a universe of some sort. The issue is to see how they interact.

David Michael Roberts (Aug 14 2023 at 03:46):

The actual point in question I'm looking at understanding is something like $\square \neg\neg \exists x (\ldots)$, where the $\square$ is necessity ranging over "possible worlds" and the $\neg\neg$ is double-negation that happens inside each possible world.

Matteo Capucci (he/him) (Aug 14 2023 at 07:52):

Maybe you already did, but have you checked the nLab page on S5 modal logic? [[necessity and possibility]]
The point of view there is that of dependent type theory, so $\square$ and $\diamondsuit$ arise as the adjoint modalities associated to the $\exists \omega \dashv \omega^* \dashv \forall \omega$, where $\omega :W \to W_0$ displays the 'equiaccessibility' relation on the type of worlds (i.e. $\omega(w) = \omega(w')$ iff $w$ is accessible from $w'$ and viceversa). It seems in this setting you should have no problems in giving semantics to your predicate?