nLab star-polycategory

Contents

Contents

Idea

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.

Definition

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):

  • A collection of objects, together with an involution operation () *(-)^* (so A **=AA^{**}=A).
  • For lists Γ\Gamma, Δ\Delta of objects, a set Hom(Γ;Δ)Hom(\Gamma;\Delta).
  • Exchange and negation structure: Two lists Γ\Gamma and Δ\Delta induce a single list Γ *,Δ\Gamma^*,\Delta by concatenating Γ *\Gamma^* with Δ\Delta. Each object-preserving-bijection Γ *,ΔΠ *,Σ\Gamma^*,\Delta\to\Pi^*,\Sigma should induce a function Hom(Γ;Δ)Hom(Π;Σ)Hom(\Gamma;\Delta)\to \Hom(\Pi;\Sigma), compatible with composition of bijections.
  • For each object AA, an identity morphism Hom(A;A)Hom(A;A).
  • For lists Γ,Δ,Π,Σ\Gamma,\Delta,\Pi,\Sigma and objects AA, a composition function
    Hom(Γ;A,Δ)×Hom(Π,A;Σ)Hom(Γ,Π;Δ,Σ)Hom(\Gamma;A,\Delta)\times Hom(\Pi,A;\Sigma)\to Hom(\Gamma,\Pi;\Delta,\Sigma)

    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 Γ 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.

  • A collection of objects, together with an involution () *(-)^* (so A **=AA^{**}=A).
  • For any list Γ\Gamma of objects, a set Hom(Γ)Hom(\Gamma) of “morphisms”.
  • Each object-preserving-bijection ΓΔ\Gamma\to \Delta should induce a function Hom(Γ)Hom(Δ)Hom(\Gamma)\to \Hom(\Delta), compatible with composition of bijections.
  • For each object AA, an identity morphism Hom(A,A *)Hom(A,A^*).
  • For lists Γ,Δ\Gamma,\Delta and objects AA, a composition function
    Hom(Γ,A)×Hom(A *,Δ)Hom(Γ,Δ)Hom(\Gamma,A)\times Hom(A^*,\Delta)\to Hom(\Gamma,\Delta)

    respecting the exchange structure and satisfying identity and associativity laws.

Examples

  • 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, A *=A opA^*=A^{\mathrm{op}}, and (using the entries-only definition) Hom(A 1,,A n)=Cat(A 1×A n,Set)Hom(A_1,\dots,A_n)=Cat(A_1\dots\times\dots A_n,\mathbf{Set}). 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 [0,1][0,1], and the involution is A *=(1A)A^*=(1-A). Hom(A 1,A n)Hom(A_1,\dots A_n) is inhabited if i=1 nA i=1\sum_{i=1}^n A_i = 1, i.e. if the list partitions the interval. Note that this polycategory is not representable, for example, we cannot combine 11 with anything except 00.

  • More generally, any effect algebra forms a thin star-polycategory in the same way. Sequences Γ\Gamma for which Hom(Γ)Hom(\Gamma) is inhabited are usually called “tests”. The tensor in the polycategorical sense is the partial monoid in the effect algebra sense.

References

Last revised on June 6, 2022 at 22:12:52. See the history of this page for a list of all contributions to it.