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.

Definition in terms of duals

Let AA be an object in a symmetric polycategory. A dual for AA comprises an object A *A^* together with a morphism Hom(A,A *;)Hom(A,A^*;-) making the induced composition Hom(Γ;A,Δ)Hom(Γ,A *;Δ)Hom(\Gamma;A,\Delta)\to Hom(\Gamma,A^*;\Delta) a bijection for all Γ\Gamma and Δ\Delta.

A symmetric star-polycategory is a symmetric polycategory in which every object has a dual.

Strict involution

In any star-polycategory there is an isomorphism A **AA^{**}\cong A for all AA. We could also require equality, A **=AA^{**}=A. 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):

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 Γ 1 *,Δ 1Γ 2 *,Δ 2\Gamma_1^*,\Delta_1 \to \Gamma_2^*,\Delta_2 and Π 1 *,Σ 1Π 2 *,Σ 2\Pi_1^*,\Sigma_1 \to \Pi_2^*,\Sigma_2 which leave the AA‘s untouched. The second, perhaps less obvious, one is that composing along AA is the same as composing along A *A^*, in that the following diagram commutes:

Hom(Γ;A,Δ)×Hom(Π,A;Σ) A Hom(Γ,Π;Δ,Σ) Hom(Γ,A *;Δ)×Hom(Π;A *,Σ) Hom(Π;A *,Σ)×Hom(Γ,A *;Δ) A * Hom(Π,Γ;Σ,Δ) \array{ Hom(\Gamma;A,\Delta) \times Hom(\Pi,A;\Sigma) &\xrightarrow{\circ_A} & Hom(\Gamma,\Pi;\Delta,\Sigma) \\ \downarrow && \downarrow \\ Hom(\Gamma,A^*;\Delta) \times Hom(\Pi;A^*,\Sigma) && \downarrow \\ \downarrow && \downarrow \\ Hom(\Pi;A^*,\Sigma) \times Hom(\Gamma,A^*;\Delta) & \xrightarrow{\circ_{A^*}} & Hom(\Pi,\Gamma;\Sigma,\Delta) }

Note that because of symmetry, we can get away with requiring composition only when AA is the first object in A,ΔA,\Delta and the last object in Π,A\Pi,A. If we included composition operations along an object AA 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 AA, hence essentially reducing them to the special case of a fixed placement (such as “first in A,ΔA,\Delta and last in Π,A\Pi,A”).

Entries only

In a star-polycategory we have natural bijections Hom(Γ;Δ)Hom(;Γ *,Δ)Hom(Γ,Δ *;)Hom(\Gamma;\Delta)\cong Hom(-;\Gamma^*,\Delta)\cong Hom(\Gamma,\Delta^*;-). 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.