Talk  Categories, Modalities, and Type Theories: Oh My
05 Mar 2021 
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^{1}! 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^{2}.
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 3045 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 halfbaked, 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^{3}, 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^{4} 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 35, 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.

Sometimes living on the west coast has its down sides… ↩

And I’m extra glad I went that week, because it was Jonathan Alcaraz’s talk on LO Groups, which led me to a problem I talked about last week ↩

Even calling it that is kind. ↩

Topology and Modality: the Topological Interpretation of FirstOrder Modal Logic, DOI: 10.1017/S1755020308080143 ↩