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: categorical logic in functor boxes

Jules Hedges (Jul 31 2024 at 18:42):

Has anybody worked out whether you can do some categorical logic in string diagrams by having a functor box for each reindexing functor and their adjoints?

Joe Moeller (Jul 31 2024 at 21:09):

I feel like Vincent Wang's thesis might be relevant, but I couldn't say for sure.

Cole Comfort (Jul 31 2024 at 21:15):

In linear logic people use functor boxes to give "string diagrams" for the ! and ? modalities.

A fibration has more structure than merely being a functor, and there are particularly nice "string diagrams" here:
https://arxiv.org/pdf/1211.1555

Jules Hedges (Aug 02 2024 at 11:57):

Joe Moeller said:

I feel like Vincent Wang's thesis might be relevant, but I couldn't say for sure.

I was Vincent's external examiner, I learned about how to do functor boxes for fibrations from him, but there's not much categorical logic in the thesis

Jules Hedges (Aug 02 2024 at 11:58):

What I had in mind is not to use a functor box for your fibration $p : E \to B$, but to use them for the functors $f^* : p^{-1} (Y) \to p^{-1} (X)$. Those reindexing functors are not fibrations, are they?