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.
Matteo Capucci (he/him) (May 02 2020 at 13:18):Does anyone know any work about the interaction of operads and logic? In particular, it seems weird nobody ever defined a "syntactic operad" for type theories, or viceversa, extracted type theories from operads.
Nathanael Arkor (May 02 2020 at 15:13):This is in fact already common. Lawvere theories, which represent universal algebras, are equivalent to cartesian operads. It's quite common to see people working with cartesian multicategories, representing sorted algebraic structures.
Nathanael Arkor (May 02 2020 at 15:13):Correspondingly, different kinds of operads correspond to different kinds of logic. Symmetric operads correspond to linear logic, for instance.
Nathanael Arkor (May 02 2020 at 15:15):Multicategories work better than categories in some ways, as you don't have to internalise the notion of context, or context extension.
Nathanael Arkor (May 02 2020 at 15:19):I think Mike Shulman's Categorical logic from a categorical point of view takes a multicategory-oriented approach to introducing the connection between logic and category theory.
Lê Thành Dũng (Tito) Nguyễn (May 02 2020 at 15:37):There is at least one recent PhD thesis on linear logic that systematically takes an operadic view on syntax: https://lipn.univ-paris13.fr/~pellissier/soutenance/manuscript.pdf
Todd Schmid (he/they) (May 04 2020 at 09:54):@Nguyễn Lê Thành Dũng (This is excellently written, so far...)