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: Polycategories with substructural codomains?

Shea Levy (Oct 30 2020 at 11:49):

Are there (non-contrived) polycategories where it's crucial to restrict some of the structural rules in the codomain? Using my intuition from sequent calculus, I can see why you might want to restrict them in the domain, but I don't see what the constraint buys you on the other side... Hoping that seeing a real example will help get a better handle on how to think about this.

Shea Levy (Oct 30 2020 at 11:55):

My current intuition, using the disjunctive sequent calculus interpretation:

• Weakening in the codomain lets you add an output wire that will never go hot
• Contraction in the codomain lets you say "If either of these two goes hot, feed the result into this input port"
• Exchange in the codomain is harder to get an intuition for... At the very least it allows any of the output wires to be paired up with an output from an adjacent polyarrow, rather than just the ones on the edges. Note that you still want to disallow crossing between adjacent polyarrows unless you have exchange in the domain as well.

I don't get what would be useful about not having one of these.