A star-polycategory is to a star-autonomous category what a multicategory is to a monoidal category. It is a polycategory in which every object has a dual. As such it is a model of classical linear logic with no connectives except negation.
There are a number of candidate definitions, depending on what we make strict.
Let be an object in a symmetric polycategory. A dual for comprises an object together with a morphism making the induced composition a bijection for all and .
A symmetric star-polycategory is a symmetric polycategory in which every object has a dual.
In any star-polycategory there is an isomorphism for all . We could also require equality, . This holds in many concrete examples, and it holds in syntactic examples that are based on negation-normal-form. The following definition is used in (Hyland, Sec 5.3):
respecting the exchange and negation structure, and satisfying the same identity and associativity laws as for an ordinary polycategory.
In the last axiom, “respecting the exchange and negation structure” has two pieces. The first, more obvious, one is that the composition functions are natural with respect to object-preserving bijections and which leave the ‘s untouched. The second, perhaps less obvious, one is that composing along is the same as composing along , in that the following diagram commutes:
Note that because of symmetry, we can get away with requiring composition only when is the first object in and the last object in . If we included composition operations along an object with arbitrary placement in these lists, then there would be an axiom asserting that these compositions are invariant with respect to permutations that rearrange the location of , hence essentially reducing them to the special case of a fixed placement (such as “first in and last in ”).
In a star-polycategory we have natural bijections . In many concrete examples these bijections are equalities. Moreover, it could be argued that in many concrete examples the explicit direction of morphisms in a two-sided polycategory isn’t meaningful. This leads us to the following one-sided or entries only definition. It corresponds to one-sided presentation of sequent calculus.
respecting the exchange structure and satisfying identity and associativity laws.
Recall that a linearly distributive category can be understood as a representable polycategory. It is star-autonomous if the corresponding polycategory is a star-polycategory.
For example, profunctors form a (weak) star-polycategory. The objects are categories, , and (using the entries-only definition) . The hom-functors are identities, and composition is given by coends.
The unit interval forms a thin star polycategory. The objects are real numbers in the interval , and the involution is . is inhabited if , i.e. if the list partitions the interval. Note that this polycategory is not representable, for example, we cannot combine with anything except .
More generally, any effect algebra forms a thin star-polycategory in the same way. Sequences for which is inhabited are usually called “tests”. The tensor in the polycategorical sense is the partial monoid in the effect algebra sense.
Last revised on July 18, 2024 at 16:23:13. See the history of this page for a list of all contributions to it.