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.
Guillaume GEOFFROY (Jun 15 2022 at 14:59):Currently, I am writing a thesis proposal and one of the subject I will tackle is linear logic as internal logic for monoidal categories and bicategories. Another one is Isbell duality.
I need some references on these subjects.
Can you help me please?
Morgan Rogers (he/him) (Jun 15 2022 at 15:26):@Thomas Seiller or @Damiano Mazza might have some recommendations for the linear logic question.
John Baez (Jun 15 2022 at 15:31):nLab and Google get you surprisingly far on such questions.
Jean-Baptiste Vienney (Jun 17 2022 at 21:27):What do you mean by linear logic as internal logic for bicategories ? All I know which relates linear logic and bicategories is the notion of linear bicategory.
Jean-Baptiste Vienney (Jun 17 2022 at 21:34):Also, the models of full linear logic are far more than monoidal categories. It's *-autonomous categories with products, coproducts, and a linear exponential comonad (named linear categories, if you replace *-autonomous by monoidal closed, but not in the same sense that linear bicategories). A good reference for categorical models of linear logic is Categorical Semantics of Linear Logic by Paul-André Melliès.
Jean-Baptiste Vienney (Jun 17 2022 at 21:48):However, writing from scratch a sequent calculus with logical rules for bicategories and then a cut elimination procedure seems doable. The fun fact would be that you have two kind of cuts. In fact it's maybe nonsensical, you can't eliminate cuts if your only logical rules are cuts.
Jean-Baptiste Vienney (Jun 17 2022 at 21:54):Finally, I don't know the relations between symmetric monoidal categories and bicategories but I'm interested by explanations to understand your project.
John Baez (Jun 17 2022 at 22:22):A symmetric monoidal category is a tetracategory with one object, one morphism and one 2-morphism, while a bicategory is a tetracategory with only identity 3-morphisms and 4-morphisms.
John Baez (Jun 17 2022 at 22:23):We have to go up to tetracategories to fit in both symmetric monoidal categories and bicategories as special cases.
Jean-Baptiste Vienney (Jun 18 2022 at 17:58):Ok, very interesting ! Maybe we could cook « higher order categorical logic » in the sense of logics for higher categories. That gives me a lot to think about!