Talk - Categories, Modalities, and Type Theories: Oh My

05 Mar 2021 - Tags: my-talks

Last week I gave a talk at CMU’s Graduate Student Workshop on Homotopy Type Theory (HoTT). You can see the schedule of talks here.

A good friend of mine from undergrad, Jacob Neumann, reached out to me about speaking here, and I super appreciate it. It was great to see some familiar faces from the HoTT group at CMU, and the talks were well worth the 8am start time¹! Jacob’s talk on Allegories was well exposited, though it was regrettably cut short before we could get to the fun modal logic interpretation. Similarly, Wes Caldwell’s talk was a return to form for HoTT! It was cool seeing some heavy duty algebraic topology recast in this language, even if the ending was a bit beyond me right now. Steve Awodey was certainly impressed by it, so I hope Wes is proud ^_^. I was upset to have missed Colin Zwanziger’s talk, but I couldn’t miss the GSS at UCR².

I felt like I should present some thoughts of my own at a seminar like this one, and the subject matter is just on the boundary of what I feel comfortable with. Since the organizers asked for a 30-45 minute talk, I decided to stay on the shorter side: “Better to remain silent and be thought a fool than to speak and remove all doubt”, you know?

One idea that had been on my mind for a little while was making sense of first order modal logic using presheaf categories. In particular, for algebraic theories, we can view a model in a presheaf category as a presheaf of models. Then if $\mathfrak{F}$ is a kripke frame for $\mathsf{S4}$, it is a preorder and thus a category in a natural way. So we should be able to use modal logic to talk about models in $\mathsf{Set}^\mathfrak{F}$.

This idea was (and is) a bit half-baked, but it was an interesting and stressful feeling to talk about ideas of my own (particularly ideas that haven’t been fully realized yet) in a talk. Particluarly a talk with so many people I respect in attendence. I’m really grateful to the organizers and the attendees for making it such a safe space for me to discuss these things, even if I’m sure a lot of what I said was obvious to many people in the room. I really miss the CMU HoTT group, and I might start attending the seminars again since they’re online anyways.

I knew my idea wasn’t fully fleshed out³, but I also knew that something like it must be right. So I took a moment to ask the audience if they knew of any references for similar ideas. I had found a paper of Awodey and Kishida⁴ which uses topological spaces and a kind of “Étale Space” version of this idea, but nothing which used presheaves directly. Thankfully, the audience gave me a veritable barrage of papers to read (many of which I’m moving to the front of my, ever increasing “to read pile”)! For the interested:

• Kishida’s Thesis
• An extension to HOL (this one was mentioned twice, so it must be good)
• Another Kishida paper (I’d actually skimmed this one already, but I’m including it for completeness)
• A 77 pager on categorical modal logic (This is one that I’m definitely going to try to get through soon)

Even if last friday was extremely long, with seminars straight through from 8am - 3pm, then teaching from 3-5, it was entirely worth it! And now, for the abstract and recording (as usual)

---

Categories, Modalities, and Type Theories: Oh my!

Category theory and logic have a tight interplay, with structured categories providing semantics for certain logics, and “internal logics” providing a useful language for speaking about structured categories. In this introductory talk we will survey both directions of this correspondence from the point of view of modal logic.

The slides are here, and the recording is below.

---