A polycategory is like a category or a multicategory, but where both the domain and the codomain of a morphism can be finite lists of objects rather than just single objects.


Relation to PROPs

A (multicolored) PROP can also be described as a polycategory; what distinguishes a polycategory from a PROP is that in a polycategory, we can only compose along one object at once. That is, we have a composition operation

D:Hom(A,B;C,D,E)×Hom(F,D,G;H)Hom(F,A,B,G;C,H,E)\circ_D \colon Hom(A,B;C,D,E) \times Hom(F,D,G; H) \to Hom(F,A,B,G; C,H,E)

but not an operation such as

B,C:Hom(A;B,C)×Hom(B,C;D)Hom(A,D).\circ_{B,C} \colon Hom(A; B,C) \times Hom(B,C; D) \to Hom(A,D).

Internal logic

Polycategories provide a natural categorical semantics for linear logic.

Revised on January 5, 2014 10:28:15 by heisenbug? (