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.
Jean-Baptiste Vienney (Nov 10 2022 at 17:56):Do we have a framework which gives a definition of what is a categorical doctrine / a logic and is able to explain what it means for such a system to have cut elimination ( to have a coherence theorem?)? Examples of categorical doctrines / logics should include: monoidal categories = multiplicative linear logic without duality and exchange (in this case the coherence theorem is the one of MacLane), symmetric monoidal categories = multiplicative linear logic without duality (again coherence by MacLane), cartesian categories, cartesian closed categories = intuitionnistic logic, *-autonomous categories = multiplicative linear logic ...
John Baez (Nov 10 2022 at 18:05):The old idea of a doctrine as a pseudomonad on Cat is able to handle some of your examples - like monoidal, symmetric monoidal categories and cartesian categories - but not all of them, because it can't handle categories with contravariant operations, like cartesian closed categories or *-autonomous categories.
John Baez (Nov 10 2022 at 18:06):There are various ways to tackle this problem, but probably @Mike Shulman could explain them better than me.
Jean-Baptiste Vienney (Nov 10 2022 at 18:07):And what about cut elimination or coherence theorem?
Ivan Di Liberti (Nov 10 2022 at 18:15):No, we do not have it. For some of us, this is a research program, which is the reason why I won't discuss it in a forum.
Jean-Baptiste Vienney (Nov 10 2022 at 19:19):Are there some issues with what you did in your paper Context, Judgement, Deduction? You can indicate me another communication support if necessary :blush:
Mike Shulman (Nov 11 2022 at 20:08):I have given a bit of thought to what it would mean for an abstract notion of doctrine/theory to have cut-elimination. It's a bit tricky because it generally involves working with presentations rather than fully semantically incarnated theories like monads. Probably the most suggestive results along these lines that have been worked out completely are those like my paper with Licata and Riley on modal and substructural logics, which says essentially that any doctrine that can be described by a cartesian 2-multicategory admits a syntax with cut-elimination.
Jean-Baptiste Vienney (Nov 11 2022 at 21:04):I like the syntactic approach. It's the kind of things I was looking for. I'll clearly take a look at this.