Polycategory

A polycategory is like a Multicategory that can have multiple inputs and outputs.

Explicitly, a polycategory $\mathcal{C}$ consists of

• A type of objects $\mathcal{C}_{0}:\mathsf{U}{}$
• A type of polymorphisms $(-)\Rightarrow(-):\mathcal{C}_{0}^{*}\to\mathcal{C}_{0}^{*}\to\mathsf{U}{}$ indexed by lists of objects
• For every object $X$, an identity polymap $[X]\Rightarrow[X]$
• For all morphisms $f:\Theta_{1},X,\Theta_{2}\Rightarrow\Psi$ and $g:\Gamma\Rightarrow\Delta_{1},X,\Delta_{2}$, a composite

  $\par f\circ g:\Theta_{1},\Gamma,\Theta_{2}\Rightarrow\Delta_{1},\Psi,\Delta_{2}\par$

Some authors impose a further condition that some lists must be empty when performing composition, which leads to the notion of a planar polycategory.

Properties

• Polycategories are a natural place to discuss the semantics of Sequent Calculi; composition in a polycategory essentially gives you a Cut Rule for a Substructural Type Theory.