Theory and Applications of Categories, Vol. 10, No. 17, 2002, pp. 424–460.

ENTROPIC HOPF ALGEBRAS AND MODELS OF NON-COMMUTATIVE LOGIC

RICHARD F. BLUTE, FRANÇOIS LAMARCHE, PAUL RUET

ABSTRACT. We give a definition of categorical model for the multiplicative fragment of non-commutative logic. We call such structures entropic categories. We demonstrate the soundness and completeness of our axiomatization with respect to cut-elimination. We then focus on several methods of building entropic categories. Our first models are constructed via the notion of a partial bimonoid acting on a cocomplete category. We also explore an entropic version of the Chu construction, and apply it in this setting.

It has recently been demonstrated that Hopf algebras provide an excellent framework for modeling a number of variants of multiplicative linear logic, such as commutative, braided and cyclic. We extend these ideas to the entropic setting by developing a new type of Hopf algebra, which we call entropic Hopf algebras. We show that the category of modules over an entropic Hopf algebra is an entropic category (possibly after application of the Chu construction). Several examples are discussed, based first on the notion of a bigroup. Finally the Tannaka-Krein reconstruction theorem is extended to the entropic setting.

1. Introduction

Non-commutative logic, NL for short, was introduced by Abrusci and the third author in [2, 28]. It generalizes Girard’s commutative linear logic [17] and Yetter’s cyclic linear logic [31], a classical conservative extension of the Lambek calculus [22].

We consider here the multiplicative fragment of NL, which contains the main novelties. Formulas of NL are built from the following connectives:

conjunction disjunction
commutative times ⊗ par ⅋
non-commutative next ⊙ sequential ▽

The fragment of NL restricted to ⊗ and ⅋ is commutative LL, and the fragment restricted to ⊙ and ▽ is cyclic non-commutative LL. In purely non-commutative LL, cyclicity amounts to two equivalent hypotheses: admit cyclic permutations or have a single negation. In NL, sequents are partially ordered sets of formula occurrences, the partial order imposing a constraint on possible commutations (between the flat orders,

This work has been partly carried out while the third author was at McGill University, (Montréal), supported by an INRIA fellowship.

Received by the editors 2001 June 15 and, in revised form, 2002 September 2. Transmitted by Susan Niefield. Published on 2002 October 11. 2000 Mathematics Subject Classification: 03F07,03F52,18A15, 18D10, 57T05. Key words and phrases: Linear logic, monoidal categories, Hopf algebras. \begin{matrix}c \\ ◯ \end{matrix} Richard F. Blute, François Lamarche, Paul Ruet, 2002. Permission to copy for private use granted.

ENTROPIC HOPF ALGEBRAS AND MODELS OF NON-COMMUTATIVE LOGIC 425

corresponding to the commutative logic, and the linear orders which represent the purely non-commutative logic). The cyclicity of NL is controlled by the structural rules seesaw, coseesaw and entropy, which allow for a limited form of the exchange rule. The sequent calculus for multiplicative NL is recalled in Appendix A. Observe that coseesaw is taken as a primitive rule, even though as far as provability is concerned, it is derivable from entropy; however, it has a very different intuition (seesaw and coseeesaw are inverses of each other) and, as we shall see, a different categorical interpretation.

When one considers the invariant of posets under the bijective action of seesaw, together with its inverse coseeesaw, one obtains an order variety [2, 28]. Using the terminology of Joyal’s species of structures [18], one sees that posets are derivatives of order varieties, in analogy with linear orders, which are derivatives of cyclic permutations. On the other hand, entropy irreversibly weakens the order; it implies that the commutative tensor ⊗ is stronger than the non-commutative one ⊙. For a more substantial survey on NL, see [2, 28].

In the present paper, we investigate the definition of categorical models of multiplicative NL (section 2). These are categories which have two ∗-autonomous structures [3, 4] together with a monoidal natural transformation, called entropy, from one tensor product to the other. The entropy map is the most interesting part of the definition, and for this reason, we call such categories entropic. It is this monoidal transformation which dictates the interaction between the two monoidal structures. Section 2 demonstrates the usual structure necessary for a denotational semantics. We give an interpretation of multiplicative NL and demonstrate that our interpretation is invariant under reduction (cut-elimination).

The remainder of the paper is devoted to the construction of entropic categories (sections 3 and 4). One important class of methods for constructing symmetric monoidal categories (SMCs) can be summarized as follows. Take a simple monoid-like structure and “expand” it to a whole category, the monoid-like structure being used, naturally, to define the tensor product of the category. This idea, in the entropic case, leads to the notion of a partial bimonoid, discussed below.

Another crucial class of monoidal categories arises from the representation theory of Hopf algebras. Categories of representations of Hopf algebras have proven to be fundamental in many branches of mathematics, from quantum physics to combinatorics. Recently, they have also been used in [6, 8, 9] to construct various models of (multiplicative) LL. In the present setting, the notions of non-commutative logic and entropic categories lead naturally to new classes of Hopf algebras, which we call entropic and coentropic. One of the chief purposes of this paper is to study these new Hopf algebraic notions. In particular, we provide a number of examples. The most familiar example of a Hopf algebra is the vector space generated by the elements of a group. In the entropic setting, one has the notion of a bigroup, which is essentially a set with two related group structures.

A possible class of examples arises from the bicrossed product construction, and indeed we would suggest that non-commutative logic may provide a natural logical framework for the analysis of this construction. Further we extend the familiar Tannaka-Krein reconstruction theorems to the entropic setting (Section 5), which demonstrates that our notion of entropic category is indeed the correct one for the semantics of non-commutative logic.

One of the crucial difficulties in modeling NL is in the negation. NL has the property that the negation (or duality) for the two ∗-autonomous structures is the same. Constructing monoidal closed categories with an involutive duality is problematic enough in general, but the above observation adds an additional layer of difficulty. However, the now familiar Chu construction can be adapted to solve this problem perfectly. In essence our Hopf algebraic models will initally only be intuitionistic, in that they will have the appropriate closed structures, but not an involutive duality. Applying the Chu construction to such categories yields entropic categories as desired, as is also the case for the categories obtained from partial bimonoids. The appropriate form of the Chu construction is presented in detail, the reason being that what was first thought to be a simple exercise turned out to reveal unexpected subtleties about the nature of cyclicity and its relationship with monoidal biclosed (or bi-autonomous) structure.

Finally, we note that a notion similar to the notion of entropic category can be obtained as an instance of the more general notion of logic of a linear functor, as defined in [7]. A linear functor between two ∗-autonomous categories is in fact a pair of functors, one of which is monoidal with respect to the tensor, and the other comonoidal with respect to the par. The two functors are then related by a natural transformation satisfying various coherence conditions. The paper [7] provides a logical syntax for the analysis of linear functors. Our definition of entropic category is roughly equivalent to having a single category with two ∗-autonomous structures, one commutative and one cyclic related by a linear endofunctor, whose two component functors are the identity. Then the entropy map of our definition is obtained as the above mentioned natural transformation.

Acknowledgements

We thank Robin Cockett and Robert Seely who were involved in some of our early discussions, and Michael Barr for fruitful discussions on this work. The first author would like to thank the Institut de Mathématiques de Luminy for their hospitality; much of this work was done during his stay there. The third author benefited from an INRIA post-doctoral fellowship; he would like to thank the Mathematics Departments of McGill University and University of Ottawa for their hospitality.

2. Entropic categories

Intuitively, an entropic category will be a category C equipped with two ∗-autonomous structures, one symmetric and the other cyclic, related by a monoidal natural transformation corresponding to entropy. We first need some preliminaries on cyclic ∗-autonomous categories. Such a category can be described as a monoidal biclosed (or biautonomous) category which is equipped with a cyclic dualizing object. There are two qualifiers here, cyclic and dualizing, and they are actually two independent concepts. First the more familiar one:

2.1. Definition. An object ⊥ in a biclosed category C is said to be dualizing if the standard maps A → (⊥^{•}− A) −^{•} ⊥ and A → ⊥^{•}− (A −^{•} ⊥) obtained by taking the exponential adjoints of the evaluation maps of A −^{•} ⊥ and ⊥^{•}− A, are isomorphisms for all A. When this happens we say C is ∗-bi-autonomous.

The concept of a cyclic object in a category generalizes the one given by Yetter [31] for posets:

2.2. Proposition. Let (C, ⊙) be a bi-autonomous category which is a poset, and ⊥ be an object of C. The following are equivalent:

• For any object A in C, A −^{•} ⊥ = ⊥^{•}− A.

• For any objects A_{1}, …, A_{n} in C, A_{1} ⊙ … ⊙ A_{n} ⩽ ⊥ if and only if A_{n} ⊙ A_{1} ⊙ … ⊙ A_{n−1} ⩽ ⊥.

We could not find the following definition in the literature, although it is closely related to the discussion on cyclicity given in [11]. In a sense the definition for cyclicity given in this latter work is more general than ours since it is done in a bi-categorical (as opposed to monoidal) framework, but at the same time our own definition does not seem to be immediately derivable from it because [11] presupposes the existence of a par (in the form of another monoidal structure, related to the tensor through a well-known law) in all the constructions.

2.3. Definition. An object ⊥ in a biclosed category is said to be cyclic if it is equipped with a natural equivalence θ: (−) −^{•} ⊥ → ⊥^{•}− (−), which is required to satisfy the condition: if χ_{A,B}: Hom(A ⊙ B, ⊥) → Hom(B ⊙ A, ⊥) is the bijection (obviously natural in A, B), defined by

Hom(A ⊙ B, ⊥) ≅ Hom(B, A −^{•} ⊥) ≅ Hom(B, ⊥^{•}− A) ≅ Hom(B ⊙ A, ⊥),

we require that Hom(B, ⊥) ≅ Hom(1 ⊙ B, ⊥) ^{χ_{1,B}}^{}Hom(B ⊙ 1, ⊥) ≅ Hom(B, ⊥) is the identity (we call this condition compatibility with unit), and that

[figure: Hom(A ⊙ (B ⊙ C), ⊥); χ_{A,B⊙C}; Hom((B ⊙ C) ⊙ A, ⊥); ass; Hom(B ⊙ (C ⊙ A), ⊥)]

[figure: Hom((A ⊙ B) ⊙ C, ⊥); ass; χ_{A⊙B,C}; Hom(C ⊙ (A ⊙ B), ⊥); ass; Hom((C ⊙ A) ⊙ B, ⊥); χ_{C⊙A,B}]

commutes (we call this condition compatibility with associativity).

For example the terminal object is always cyclic. Also, if the monoidal structure is equipped with a symmetry, every object of the category becomes cyclic. Notice that compatibility with unit is equivalent to the stipulation that the following commutes:

[figure: 1 −^{•} ⊥; θ_{1}; ⊥^{•}− 1; ⊥; ∼; = = = = = = = = =; ⊥; ∼]

Now assume that in the diagram above, A is the tensor unit. By using the unit isomorphisms X ⊙ 1 ≅ X and 1 ⊙ X ≅ X, we see that compatibility with associativity implies the following diagram:

[figure: Hom(B ⊙ C, ⊥); Hom((1 ⊙ B) ⊙ C, ⊥); ass; Hom(1 ⊙ (B ⊙ C), ⊥)]

[figure: Hom(C ⊙ B, ⊥); χ_{B,C}; Hom(C ⊙ (1 ⊙ B), ⊥); χ_{1⊙B,C}; Hom((B ⊙ C) ⊙ 1, ⊥); χ_{1,B⊙C}]

[figure: Hom((C ⊙ 1) ⊙ B, ⊥); ass; χ_{C⊙1,B}; Hom(B ⊙ (C ⊙ 1), ⊥); ass]

[figure: Hom(C ⊙ B, ⊥); Id; = = = = =; Hom(C ⊙ B, ⊥); χ_{C,B}; Hom(B ⊙ C, ⊥)]

where the top left square and the bottom right square commute because of naturality, and the bottom left “rectangle” does because of standard facts about associativity and unit. Composing the top horizontal arrow with the right vertical arrow of this diagram gives the identity on Hom(B ⊙ C, ⊥), because of compatibility with unit. So this diagram should be read as the equation χ_{C,B} ∘ χ_{B,C} = Id, in other words, we have that χ is an involution, a negated version of the symmetry in a monoidal category. Let us call this equation the involution property of χ.

2.4. Proposition. Let θ: (−) −^{•} ⊥ → ⊥^{•}− (−) be a natural equivalence and χ be obtained from θ in the same way as above. Then the first condition below implies the second:

• χ has the involution property • The diagram

\begin{matrix}A & = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = & A \\ (⊥^{•}− A) −^{•} ⊥ & & \overline{θ_{A} −^{•} ⊥^{}} & (A −^{•} ⊥) −^{•} ⊥ & \overline{θ_{A −• ⊥}^{}} & ⊥^{•}− (A −^{•} ⊥) & \end{matrix}

commutes for every A.

Furthermore, if ⊥ is dualizing, then the two conditions are equivalent.

The proof is a long computation. The second of these properties is what Rosenthal [27] (in the case ⊥ is a dualizing object) calls cyclicity. In light of what we have seen, there seem to be two different ways of defining cyclicity for a pair (⊥, θ) (where ⊥ is dualizing): a strong way, which is compatibility with unit combined with compatibility with associativity, and a seemingly weaker way, which is the involution property. We have good reasons to believe that these two definitions are not equivalent. Notice that the involution property means that there is a coherent isomorphism between all the different possible ways of defining the “n-fold negation” of A, using all possible combinations of the two implications.

2.5. Definition. We say a category C is cyclic ∗-autonomous when it is equipped with a cyclic dualizing object.

Naturally a more correct terminology would be cyclic ∗-biautonomous. We now introduce the main definition of the paper.

2.6. Definition. An entropic category is a category C equipped with:

1. two functors ⊙, ⊗: C × C → C and an object 1 in C such that (C, ⊙, 1) is a monoidal category and (C, ⊗, 1) is a symmetric monoidal category (with same unit);

2. an equivalence (−)^{∗}: C → C^{op} making (C, ⊙, 1) cyclic ∗-autonomous and (C, ⊗, 1) symmetric ∗-autonomous, with ⊥ = 1^{∗};

3. a monoidal natural transformation ε: ⊗ →^{·} ⊙, called entropy, which is compatible with the symmetry in the following sense: for any f: A ⊙ B → ⊥ in C the diagram

[figure: B ⊗ A; c; A ⊗ B; ε; A ⊙ B; B ⊙ A; ε; χ(f); ⊥; f]

commutes.

The monoidality of ε amounts to the following commutations:

[figure: A ⊗ 1; ε; A ⊙ 1; 1 ⊗ A; ε; 1 ⊙ A; A; ∼; = = = = = = = = =; A; ∼; A; ∼; = = = = = = = = =; A; ∼]

A ⊗ (B ⊗ C) {= \atop =} A ⊗ (B ⊗ C) \overline{a_{}}(A ⊗ B) ⊗ C {= \atop =} (A ⊗ B) ⊗ C

[figure: A ⊙ (B ⊗ C); ε; A ⊗ (B ⊙ C); Id ⊗ ε; (A ⊗ B) ⊙ C; ε; (A ⊙ B) ⊗ C; ε ⊗ Id]

[figure: A ⊙ (B ⊙ C); Id ⊙ ε; {= \atop =}; A ⊙ (B ⊙ C); ε; a; (A ⊙ B) ⊙ C; ε ⊙ Id; {= \atop =}; (A ⊙ B) ⊙ C; ε]

Compatibility with associativity and unit are not necessary in general, but these rules ensure that the categorical interpretation of a sequent is invariant under all possible ways of doing cyclic exchange on it; for example if you have a four-formula sequent and do cyclic exchange four times on it, you get the same map as you started with. Monoidality of ε is actually not required for cut-elimination either, but it is a convenient assumption which identifies, for instance, proofs which differ only in the order of application of entropy.

We will assume that the natural isomorphism (−)^{∗} ≅ ^{∗}(−) is the identity.

2.7. Definition. The duals of ⊙, ⊗ and 1 are respectively denoted ▽, ⅋ and ⊥. Note the reversed order in the case of ▽: ▽ is the functor defined on objects by A▽B = (B^{∗} ⊙A^{∗})^{∗}. The internal homs are A ⊸ B = A^{∗} ⅋ B, A −^{•} B = A^{∗} ▽ B and B^{•}− A = B ▽ A^{∗}. The composite

Hom(1, A ⅋ B) →^{∼} Hom(A^{∗}, B) →^{∼} Hom(1, A ▽ B)

is called seesaw, and the inverse map is called coseesaw.

Let us recall the following lemma, which holds by naturality of the commutativity constraint in any symmetric ∗-autonomous category:

2.8. Lemma. The following diagram commutes in any symmetric ∗-autonomous category:

Hom(1, (A ⊗ B)^{∗}) \overline{c_{B,A}^{∗} ∘ −_{}}Hom(1, (B ⊗ A)^{∗})

[figure: Hom(A, B^{∗}); ∼; (−)^{∗}; Hom(B, A^{∗}); ∼]

By now it is a standard observation that compact closed categories [20] are a degenerate model of multiplicative linear logic in which the tensor and par structures are equated. Thus they can also be viewed as ∗-autonomous categories with an additional isomorphism. It turns out that in certain algebraic settings, the more natural object of study is the notion of compact closed categories, which have a canonical trace on them. This is especially true of the Tannaka-Krein reconstruction theorems [25], which we shall generalize to the entropic setting later in the paper. With this in mind, we present the definition of entropic compact closed category.

2.9. Definition. An entropic compact closed category is a category C with two monoidal structures (C, ⊗, 1) and (C, ⊙, 1), the first of which being symmetric, a function (−)^{∗} on objects, and morphisms

μ_{1} : V ⊗ V^{∗} → 1
ν_{1} : 1 → V^{∗} ⊗ V
μ_{2} : V ⊙ V^{∗} → 1
ν_{2} : 1 → V^{∗} ⊙ V.

The pairs μ_{1}, ν_{1} and μ_{2}, ν_{2} must each satisfy the usual adjunction triangles as in [20]. Finally, we require a monoidal transformation ε: ⊗ →^{·} ⊙ as above.

We can prove that the functor (−)^{∗} is then involutive. We leave it to the reader to verify that an entropic compact closed category is indeed entropic. We will see examples of such categories when we consider finite-dimensional representations of the algebraic structures considered later in the paper.

2.10. Interpretation of multiplicative NL. Let C be an entropic category and ⟦−⟧_{C} be a valuation assigning an object ⟦p⟧_{C} of C to each positive propositional symbol p. ⟦−⟧_{C} is extended to all formulas of MNL in the obvious way and the interpretation of a sequent is defined inductively by: ⟦Γ, Δ⟧_{C} = ⟦Γ⟧_{C} ⅋ ⟦Δ⟧_{C} and ⟦Γ; Δ⟧_{C} = ⟦Γ⟧_{C} ▽ ⟦Δ⟧_{C}. When the category C considered is clear from the context we shall omit the subscripts and write ⟦−⟧.

For each MNL proof π of a sequent ⊢ ω, we define by induction a morphism ⟦π⟧: 1 → ⟦ω⟧ in C as follows:

• π is:

⊢ A^{⊥}, A

⟦π⟧ is the image of the identity Id_{⟦A⟧}^{∗} by the isomorphism

Hom(⟦A⟧^{∗}, ⟦A⟧^{∗}) →^{∼} Hom(1, (⟦A⟧^{∗} ⊗ ⟦A⟧)^{∗})
= Hom(1, ⟦A^{⊥} ⅋ A⟧).

• π ends with an application of the associativity of (−, −) or (−; −), or with an application of the commutativity of (−, −): this case is straightforward.

• π is:

⊢ Γ, Δ ; seesaw ; ⊢ Γ; Δ  or  [figure: π_{1}] ; ⊢ Γ; Δ ; coseesaw. ; ⊢ Γ, Δ

⟦π⟧ is the image of ⟦π_{1}⟧: 1 → ⟦Γ⟧ ⅋ ⟦Δ⟧ = (⟦Δ⟧^{∗} ⊗ ⟦Γ⟧^{∗})^{∗} by seesaw or the image of ⟦π_{1}⟧: 1 → ⟦Γ⟧ ▽ ⟦Δ⟧ = (⟦Δ⟧^{∗} ⊙ ⟦Γ⟧^{∗})^{∗} by coseesaw (Definition 2.7).

• π is:

⊢ (Γ; Δ); Σ ; entropy. ; ⊢ (Γ, Δ), Σ

⟦π⟧ is the image of ⟦π_{1}⟧: 1 → (⟦Γ⟧ ▽ ⟦Δ⟧) ▽ ⟦Σ⟧ = (⟦Σ⟧^{∗} ⊙ (⟦Γ⟧ ▽ ⟦Δ⟧)^{∗})^{∗} by the map

Hom(1, (⟦Σ⟧^{∗} ⊙ (⟦Γ⟧ ▽ ⟦Δ⟧)^{∗})^{∗}) →^{∼} Hom(⟦Σ⟧^{∗}, ⟦Γ⟧ ▽ ⟦Δ⟧)
→^{ε^{∗}∘−} Hom(⟦Σ⟧^{∗}, ⟦Γ⟧ ⅋ ⟦Δ⟧)
→^{∼} Hom(1, (⟦Σ⟧^{∗} ⊗ (⟦Γ⟧ ⅋ ⟦Δ⟧)^{∗})^{∗})
= Hom(1, (⟦Γ⟧ ⅋ ⟦Δ⟧) ⅋ ⟦Σ⟧).

• π is:

⊢ Γ[A]  ⊢ A^{⊥}, Δ cut. ⊢ Γ[Δ]

⟦π_{2}⟧ induces a morphism ϕ: ⟦A⟧ → ⟦Δ⟧, whence a morphism Γ[ϕ]: ⟦Γ[A]⟧ → ⟦Γ[Δ]⟧ defined in the obvious way by induction on the context Γ[ ] (if Γ[ ] = Γ_{1}[ ]; Γ_{2} then Γ[ϕ] = Γ_{1}[ϕ] ▽ Id_{⟦Γ_{2}⟧}, etc.), and ⟦π⟧ is the composite

[figure: 1; ⟦π_{1}⟧; ⟦Γ[A]⟧; Γ[ϕ]; ⟦Γ[Δ]⟧.]

The same argument applies for the seven variants of the cut rule. Note that the cut rules given in Appendix A are redundant: for instance, a context Γ[A] may itself be of the form (Γ, A), so we have to verify that, when there is an ambiguity on which cut rule has been applied, the interpretations are the same. Such an ambiguity occurs for a cut between Γ[A] and Δ[A^{⊥}] exactly when Γ[Δ] = Δ[Γ]. (This implies in particular that both Γ[A] and Δ[A^{⊥}] have the cut formula “outside” the context.) The point is that the only possibilities are:

Γ[−] = (Γ, −) and Δ[−] = (−, Δ)
Γ[−] = (Γ; −) and Δ[−] = (−; Δ)
Γ[−] = (−, Γ) and Δ[−] = (Δ, −)
Γ[−] = (−; Γ) and Δ[−] = (Δ; −)

and it is standard for ∗-autonomous categories to have the two possible interpretations equal. For instance, in the first case, the two morphisms (Id_{⟦Γ⟧} ⅋ ϕ_{2}) ∘ ⟦π_{1}⟧ and (ϕ_{1} ⅋ Id_{⟦Δ⟧}) ∘ ⟦π_{2}⟧: 1 → ⟦Γ⟧ ⅋ ⟦Δ⟧, with ϕ_{2} : ⟦A⟧ → ⟦Δ⟧, ϕ_{1} : ⟦A⟧^{∗} → ⟦Γ⟧ as above, are equal.

• π is:

⊢ Γ; A  ⊢ Δ; B ⊙. ⊢ (Δ; Γ); A ⊙ B

By induction, we have morphisms

\begin{matrix}⟦π_{1}⟧: 1 → (⟦A⟧^{∗} ⊙ ⟦Γ⟧^{∗})^{∗} & and \\ ⟦π_{2}⟧: 1 → (⟦B⟧^{∗} ⊙ ⟦Δ⟧^{∗})^{∗}. \end{matrix}

⟦π_{1}⟧ and ⟦π_{2}⟧ induce morphisms ϕ: ⟦A⟧^{∗} → ⟦Γ⟧ and ψ: ⟦B⟧^{∗} → ⟦Δ⟧. Then ψ ▽ ϕ: ⟦A ⊙ B⟧^{∗} → ⟦Δ⟧ ▽ ⟦Γ⟧ gives the required morphism

⟦π⟧: 1 → (⟦A ⊙ B⟧^{∗} ⊙ (⟦Δ⟧ ▽ ⟦Γ⟧)^{∗})^{∗} = (⟦Δ⟧ ▽ ⟦Γ⟧) ▽ ⟦A ⊙ B⟧.

• π is:

⊢ Γ, A  ⊢ Δ, B ⊗. ⊢ (Δ, Γ), A ⊗ B

Similar argument, replacing ⊙ by ⊗ and ▽ by ⅋.

• π is:

\begin{aligned}⊢ Γ; (A; B) \\ & ▽ \\ ⊢ Γ; A ▽ B \end{aligned}  or  [figure: π_{1}] ; ⊢ Γ, (A, B) ; ⅋. ; ⊢ Γ, A ⅋ B

Trivially ⟦π⟧ = ⟦π_{1}⟧.

• π is:

\begin{aligned}& . \\ ⊢ 1 \end{aligned}

⟦π⟧ = id_{1}.

• π is:

\begin{aligned}⊢ Γ \\ & ⊥. \\ ⊢ Γ, ⊥ \end{aligned}

⟦π⟧ is obtained using the unit isomorphism. 2.11. Theorem (Invariance under reduction). Let C be an entropic category, ⟦−⟧_{C} a valuation and π an MNL proof. If π reduces to π′, then ⟦π⟧_{C} = ⟦π′⟧_{C}. Proof. It is enough to prove the result for one reduction step π ⇝ π′:

• Identity:

\begin{aligned}⊢ Γ[C] & ⊢ C^{⊥}, C \\ & cut \\ ⊢ Γ[C] \end{aligned} ⇝ [figure: π_{1}] ; ⊢ Γ[C]

⟦π⟧ = ϕ ∘ ⟦π_{1}⟧ where ϕ is the image of the identity Id_{⟦C^{⊥}⟧} under the composite

Hom(⟦C⟧^{∗}, ⟦C⟧^{∗}) ≅ Hom(1, ⟦C ⅋ C^{⊥}⟧)
→^{c^{∗}∘−} Hom(1, ⟦C^{⊥} ⅋ C⟧)
≅ Hom(⟦C⟧, ⟦C⟧).

By Lemma 2.8, this is Id_{⟦C⟧}, and therefore ⟦π⟧ = ⟦π_{1}⟧ = ⟦π′⟧.

• Associativity:

⊢ Θ, C^{⊥}  ⊢ Π[Γ; (Δ[C]; Σ)] a1 ⊢ Π[(Γ; Δ[C]); Σ] cut ⊢ Π[(Γ; Δ[Θ]); Σ] ⇝ [figure: π_{1}; ⊢ Θ, C^{⊥}; π_{2}; ⊢ Π[Γ; (Δ[C]; Σ)]] cut ⊢ Π[Γ; (Δ[Θ]; Σ)] a1 ⊢ Π[(Γ; Δ[Θ]); Σ]

The hom-sets Hom(1, A ⅋ B) and Hom(1, A ▽ B) are in bijection, so one replaces ⟦π_{1}⟧ : 1 → Θ ⅋ C^{⊥} by ⟦π′_{1}⟧ : 1 → Θ ▽ C^{⊥}, and the result follows immediately from the naturality of the associativity constraints (cut-elimination for cyclic LL).

• Commutativity:

[figure: π_{1}; ⊢ Θ, C^{⊥}; π_{2}; ⊢ Π[Γ, Δ[C]]; com; ⊢ Π[Δ[C], Γ]] cut ⊢ Π[Δ[Θ], Γ] ⇝ [figure: π_{1}; ⊢ Θ, C^{⊥}; π_{2}; ⊢ Π[Γ, Δ[C]]] cut ⊢ Π[Γ, Δ[Θ]] com ⊢ Π[Δ[Θ], Γ]

The result follows from the naturality of the commutativity constraint.

• Seesaw, coseesaw:

⊢ Θ, C^{⊥}  ⊢ Γ, Δ[C] ; seesaw ; ⊢ Γ; Δ[C] cut ⊢ Γ; Δ[Θ] ⇝ [figure: π_{1}; ⊢ Θ, C^{⊥}; π_{2}; ⊢ Γ, Δ[C]] cut ⊢ Γ, Δ[Θ] seesaw ⊢ Γ; Δ[Θ]

⊢ Θ, C^{⊥}  ⊢ Γ; Δ[C] ; coseesaw ; ⊢ Γ, Δ[C] cut ⊢ Γ, Δ[Θ] ⇝ [figure: π_{1}; ⊢ Θ, C^{⊥}; π_{2}; ⊢ Γ; Δ[C]] cut ⊢ Γ; Δ[Θ] coseesaw ⊢ Γ, Δ[Θ]

The result follows from the naturality of the seesaw map Hom(1, (A ⊗ B^{∗})^{∗}) →^{∼} Hom(1, (A ⊙ B^{∗})^{∗}).

• Entropy:

⊢ Θ, C^{⊥}  ⊢ Γ; Δ[C]; Σ ; entropy ; ⊢ Γ, Δ[C], Σ cut ⊢ Γ, Δ[Θ], Σ ⇝ [figure: π_{1}; ⊢ Θ, C^{⊥}; π_{2}; ⊢ Γ; Δ[C]; Σ] cut ⊢ Γ; Δ[Θ]; Σ entropy ⊢ Γ, Δ[Θ], Σ

The result follows from the naturality of ε.

• Next:

⊢ Θ, C^{⊥} \begin{aligned}⊢ Γ[C]; A & ⊢ Δ; B \\ & ⊙ \\ ⊢ (Δ; Γ[C]); A ⊙ B \end{aligned} cut ⊢ (Δ; Γ[Θ]); A ⊙ B ⇝ [figure: π_{1}; ⊢ Θ, C^{⊥}; π_{2}; ⊢ Γ[C]; A; cut; ⊢ Γ[Θ]; A; π_{3}; ⊢ Δ; B] ⊙ ⊢ (Δ; Γ[Θ]); A ⊙ B

The result follows from the functoriality of ▽.

• Times: this case is similar.

• Sequential:

⊢ Θ, C^{⊥} \begin{aligned}⊢ Γ[C]; (A; B) \\ & ▽ \\ ⊢ Γ[C]; A ▽ B \end{aligned} cut ⊢ Γ[Θ]; A ▽ B ⇝ \begin{aligned}[figure: π_{1}] ; ⊢ Θ, C^{⊥} & [figure: π_{2}] ; ⊢ Γ[C]; (A; B) \\ & cut \\ ⊢ Γ[Θ]; A; B \end{aligned} ▽ ⊢ Γ[Θ]; A ▽ B

This case is trivial.

• Par: this case is similar.

• Next-Sequential:

\begin{aligned}⊢ Θ; (A; B) \\ & ▽ \\ ⊢ Θ; A ▽ B \end{aligned} \begin{aligned}⊢ Γ; B^{⊥} & ⊢ Δ; A^{⊥} \\ & ⊙ \\ ⊢ (Δ; Γ); B^{⊥} ⊙ A^{⊥} \end{aligned} cut ⊢ (Δ; Γ); Θ

⇝ [figure: π_{1}; ⊢ Θ; (A; B); π_{2}; ⊢ Γ; B^{⊥}; cut; ⊢ Θ; (A; Γ); π_{3}; ⊢ Δ; A^{⊥}] cut ⊢ Θ; (Δ; Γ) coseesaw ⊢ Θ, (Δ; Γ) com ⊢ (Δ; Γ), Θ seesaw ⊢ (Δ; Γ); Θ

We observe that coseesaw followed by commutativity and seesaw is the cyclic exchange rule, and therefore this case follows from cut-elimination in cyclic ∗-autono-mous categories.

• Times-Par: similar.

• The units are treated in a similar fashion.

3. Entropic categories and the Chu construction

3.1. Categorical generalities. Given a monoidal category (C, ⊙) it is said to be biautonomous when, for any object A both functors (−) ⊙ A and A ⊙ (−) have a right adjoint; we will denote these by A −^{•} (−) and (−)^{•}− A respectively; notice that this gives us the reversible rules

\frac{B ⊙ A → C}{A → B −^{•} C}  \frac{A ⊙ B → C}{A → C ^{•}− B}

which are easy to memorize, and compatible with the classical sequent calculus if A −^{•} B is defined as A^{⊥} ▽ B. One standard consequence of these axioms is that the associativity map gives rise to an isomorphism (A −^{•} X)^{•}− B ≅ A −^{•} (X ^{•}− B), which allows us to drop the parentheses.

If the monoidal structure is symmetric, which naturally we denote by (−) ⊗ (−), obviously we have that one of the adjoints above exists if and only if the other one does, and the two implication bifunctors are equivalent. We will nevertheless distinguish A −∘ (−) from (−) ∘− A. The reason for this is that in order to construct the natural equivalence between these two, we have to use the symmetry; in particular, the equivalence (A −∘ X) ∘− B ≅ A −∘ (X ∘− B) is independent of the existence of a symmetry. This is also compatible with the syntax, since, because we live in a basically non-commutative world, negation has to exchange the order of premises as well as de Morgan dualizing the connectives. We prefer to say that such a category is autonomous rather than symmetric monoidal closed.

If now C has two tensors that are related by an entropy ε, we get a natural map ε^{∗}: A −^{•} B → A −∘ B defined by

\frac{A ⊗ (A −^{•} B) ^{ε}^{}A ⊙ (A −^{•} B) ^{ev}^{}B}{A −^{•} B ^{}A −∘ B}

and similarly we have ε_{∗}: A^{•}− B → A ∘− B, with the property that the following commutes, whatever way the vertical maps are defined:

[figure: (A −^{•} X)^{•}− B; ∼; A −^{•} (X ^{•}− B); (A −∘ X) ∘− B; ∼; A −∘ (X ∘− B)]

which allows us to drop even more parentheses. All the above also is valid, mutatis mutandi, if the entropy ⊗ → ⊙ is replaced by a coentropy ⊙ → ⊗. And we call such categories intuitionistic entropic (resp. coentropic) categories. Note that nothing about the symmetries has been used, only the fact the the maps relating the tensors are monoidal.

The aim of this section is to construct entropic categories by means of intuitionistic entropic ones. We first give a general construction of intuitionistic examples.

3.2. Partial bimonoids. To the best of our knowledge the first person who gave a systematic method for constructing monoidal and (bi)autonomous categories was Day [12]. His method uses the technique of bimodules (in the enriched sense), and can be applied in the context of any enriched category. It is extremely general and many of the methods that have been developed since, including phase semantics [17], can be shown to be examples of it.

As a first example of the construction of entropic categories, we introduce the notion of a partial bimonoid.

3.3. Definition. A partial monoid consists of a set M, together with a partial multiplication, i.e. a partial function (−) · (−): M × M → M, which is associative, and has a unit 1. By associative, we mean that if one side of the usual equation is defined, then so is the other and they are equal. We further require that the unit be total, i.e. that the functions 1 · (−) and (−) · 1 be total. Commutativity is defined similarly to associativity.

Then a partial bimonoid is a quadruple (M, ∗, ∘, 1), where ( ∗, 1) is a partial commutative monoid structure on M, (∘, 1) a partial monoid structure on M. Note that we require that the two partial monoids share the same unit. A partial bimonoid is said to be entropic if the commutative partial operation is contained in the not-necessarily-commutative one when the two operations are viewed as subsets of M × M × M. We say that M is co-entropic if the reverse is the case.

This definition can be profitably rephrased as follows: Add to M a “zero” element z, then extend the operations on M ∪ {z} by defining m ∗ n = z, m ∘ m = z whenever they are undefined in M, along with m ∗ z = z and m ∘ z = z ∘ m = z for all m. Then to say we have a partial monoid structure is equivalent to saying the extended operations are ordinary monoid structures. Moreover, if we order M ∪ {z} by saying that z is the least element, and that the order restricted to M is discrete, it is easy to see we get ordered monoid structures in which the operations are monotone, thus simple examples of monoidal categories. Then if M is entropic (resp. co-entropic), the inequality m ∗ n ≤ m ∘ n is an entropy on (M, ≤) (resp m ∘ n ≤ m ∗ n is a co-entropy). The defining diagrams are trivial to check because we are in a poset.

Let (U, ⊗, 1) be an autonomous category which is cocomplete^{1}; in particular it has an initial object 0. We are interested in extending M′s structure to the power category U^{M}, in which an object A ∈ U^{M} is a family (A_{m})_{m∈M} of objects A_{m} ∈ U, and a morphism f: A → B is defined as usual: f = (f_{m})_{m∈M} with f_{m}: A_{m} → B_{m}. When we want to consider specific components, we use indices, i.e., U_{m}^{M}(A, B) means U(A_{m}, B_{m}).

Most of the following results are well-known, if not folklore. Our only claim to originality is working with partial monoid structures (and then this can be seen to be is an application of Day’s method) and extending to entropies and co-entropies.

1Actually it suffices that it have all coproducts

3.4. Theorem. With everything defined as above, we can define a monoidal structure on U^{M} by

(A ⊙ B)_{m} = ∑_{n∘p=m} A_{n} ⊗ A_{p}

and a symmetric one by

(A ⊗ B)_{m} = ∑_{n∗p=m} A_{n} ⊗ A_{p}.

If U is closed and complete, then U^{M} is closed for both tensor structures.

In addition suppose M is entropic. Then, given m ∈ M, we have an inclusion {(n, p) | n∗p = m} ⊆ {(n, p) | n∘p = m}. From this inclusion follows a map (A⊗B)_{m} → (A⊙B)_{m} for every m. We claim that the map (A ⊗ B) → (A ⊙ B) obtained this way is an entropy. In the same manner, if M is co-entropic, we get a co-entropy A ⊙ B → A ⊗ M.

Proof. One fruitful way to think about this is to imagine that U is a (large) commutative ring. As a matter of fact, if it is a closed category, we have that the multiplication (tensor) distributes over the sum (coproduct). So what we are doing is constructing the “ring” U[M] associated to the monoid M, except, naturally, that M is not a monoid, but two partial monoids.

The proofs that we get monoidal structures, as well as (co)entropies, are straightforward and will be omitted. Let us give the definition for the two right adjoints to ⊙. Here the symbol −∘ denotes the linear implication in U.

\begin{aligned}(C ^{•}− B)_{m} & = & ∏_{m∘p=n} B_{p} −∘ C_{n} \\ (B −^{•} C)_{m} & = & ∏_{p∘m=n} B_{p} −∘ C_{n}. \end{aligned}

The proof that these definitions work is a simple computation, e.g.,

U_{m}^{M}(A, C ^{•}− B) ≅ U(A_{m}, ∏_{m∘p=n} B_{p} −∘ C_{n})
≅ ∏_{m∘p=n} U(A_{m}, B_{p} −∘ C_{n})
≅ U(∑_{m∘p=n} A_{m} ⊗ B_{p}, C_{n})
≅ ((A ⊙ B)_{m}, C_{m})
≅ U_{m}^{M}(A ⊙ B, C).

The same goes for the adjoint(s) to the symmetric tensor, which are defined just as above, replacing ∘ by ∗.

These formulas should have an air of familiarity to anyone who has done phase semantics [17]. The real difficulty is in obtaining interesting partial bimonoids. The following is one naturally occurring example.

Take the set M = ℕ × ℕ, the product of non-negative integers with itself. Define a partial operation by:

(m, m′) ∘ (n, n′) = \{ \begin{matrix}(m + n, m′ + n′) if m = 0 or n′ = 0 \\ undefined otherwise. \end{matrix}

Taking (0, 0) as unit, the unit law follows easily. We have to show associativity, i.e., that ((m_{1}, m′_{1}) ∘ (m_{2}, m′_{2})) ∘ (m_{3}, m′_{3}) is defined if and only if (m_{1}, m′_{1}) ∘ ((m_{2}, m′_{2}) ∘ (m_{3}, m′_{3})) is. Suppose that both m_{1}, m′_{3} = 0. Then both sides are defined, no matter what. Suppose that both m_{1}, m′_{3} ≠ 0. Then neither side can be defined unless m_{2}, m′_{2} = 0, in which case they both are defined.

So suppose that one of them, say m_{1} ≠ 0. Then for the left side to be defined, we have to have both m′_{2} = 0, m′_{3} = 0. For the right side to be defined, we have to have m′_{2} + m′_{3} = 0, which forces m′_{2}, m′_{3} = 0. Repeating this argument with m′_{3} ≠ 0 completes the proof.

In general we see that in any product, (m_{1}, m′_{1}) ∘ (m_{2}, m′_{2}) ∘ ⋯ ∘ (m_{n}, m′_{n}) which is defined, m_{k} ≠ 0 forces m_{i} = 0, i < k, and m′_{k} ≠ 0 forces m′_{i} = 0, i > k.

We have constructed a co-entropic partial bimonoid, namely (M, +, ∘, (0, 0)). Now let (m, m′) ∗ (n, n′) be defined as:

(m, m′) ∗ (n, n′)

= \{ \begin{matrix}(m + n, m′ + n′) & if (m, m) ∘ (n, n′) = (n, n′) ∘ (m, m′) (both defined) \\ undefined & otherwise \end{matrix}

equivalently,

(m + n, m′ + n′) if and only if (m = 0 or n′ = 0) and (m′ = 0 or n = 0).

So ∗ is the largest commutative operation contained in ∘. Naturally we have to show it is associative again. It is easy to see that given a sequence (m_{1}, m′_{1})∗(m_{2}, m′_{2})∗⋯∗(m_{n}, m′_{n}), it is undefined if and only if there are j ≠ k with m_{i} ≠ 0 and m′_{j} ≠ 0. And both this condition and its negation are independent of any bracketing and ordering of the terms.

So we get that (M, ∗, ∘, (0, 0)) is an entropic partial bimonoid.

3.5. The Entropic Chu Construction. Since we now have a store of intuitionistic entropic categories, the next step is to obtain genuine (∗-autonomous) entropic categories. We will use techniques from Barr’s Chu and cyclic Chu construction [4, 5] which can be readily adapted to our situation. We will build on the observation by M. Barr [5] that the most natural road to the Chu construction and its generalizations is to start with the terminal object as a dualizer.

Given any biautonomous category with products (C, ⊙) then the category C × C^{op} has a cyclic ∗-autonomous structure, given by the following: the tensor of two objects A = (A^{+}, A^{−}) and B = (B^{+}, B^{−}) is the pair

(A^{+} ⊙ B^{+}, (B^{+} −^{•} A^{−}) × (B^{−} ^{•}− A^{+}))

A quick computation shows that for n-tuples, A_{1} ⊙ A_{2} ⊙ A_{3} ⊙ ⋯ ⊙ A_{n} is given by:

(A_{1}^{+} ⊙ A_{2}^{+} ⊙ ⋯ ⊙ A_{n}^{+}, (A_{2}^{+} ⊙ A_{3}^{+} ⊙ ⋯ ⊙ A_{n}^{+} −^{•} A_{1}^{−}) × (A_{3}^{+} ⊙ ⋯ ⊙ A_{n}^{+} −^{•} A_{2}^{−} ^{•}− A_{1}^{+})×
(A_{4}^{+} ⊙ ⋯ ⊙ A_{n} −^{•} A_{3}^{−} ^{•}− A_{1}^{+} ⊙ A_{2}^{+}) × ⋯ ×
(A_{n}^{−} ^{•}− A_{1}^{+} ⊙ A_{2}^{+} ⊙ ⋯ ⊙ A_{n−1}^{+}))

Being that we want A^{⊥} = (A^{−}, A^{+}), by duality we have:

A −^{•} B = ((A^{+} −^{•} B^{+}) × (B^{−} ^{•}− A^{−}) , B^{−} ⊙ A^{+}).

3.6. Proposition. Given the definitions above, the standard adjunctions

Hom(A ⊙ B, C) ≅ Hom(A, C ^{•}− B) ≅ Hom(B, A −^{•} C)

hold, and the object (⊤, 1) (where ⊤ is terminal in C ) is a cyclic dualizing object.

The proof is standard [5]. For instance, the correspondence

\begin{matrix}Hom & ((A^{+} ⊙ B^{+}, (B^{+} −^{•} A^{−}) × (B^{−} ^{•}− A^{+})) , (C^{+}, C^{−})) & ≅ \\ Hom & ((B^{+}, B^{−}) , ((A^{+} −^{•} C^{+}) × (C^{−} ^{•}− A^{+}) , C^{−} ⊙ A^{+}) & ) \end{matrix}

is obtained by noticing that both hom-sets above are naturally isomorphic to

Hom_{C}(A^{+} ⊙ B^{+}, C^{+}) × Hom_{C}(B^{+} ⊙ C^{−}, A^{−}) × Hom_{C}(C^{−} ⊙ A^{+}, B^{−}).

For the cyclicity of (⊤, 1), notice that Hom_{C×C^{op}} (A ⊙ B ⊙ C, (⊤, 1)) is isomorphic to

Hom (1, (B^{+} ⊙ C^{+} −^{•} A^{−}) × (C^{+} −^{•} B^{−} ^{•}− A^{+}) × (C^{−} ^{•}− A^{+} ⊙ B^{+})) ,

which is invariant under cyclic permutations, being isomorphic to

Hom_{C}(B −^{•} C, A) × Hom_{C}(C −^{•} A, B) × Hom_{C}(A −^{•} B, C).

3.7. Proposition. Let there be an additional autonomous structure (⊗, −∘ , ∘−) on C and an entropy ⊗ → ⊙. Then, definining (⊗, −∘ , ∘−) on C × C^{op} just as we did above for (⊙, −^{•} , ^{•}−), mutatis mutandi, we get an entropic category structure on C × C^{op}.

Given what we have said, everything should be straightforward. Notice that the entropy reads as

(A^{+} ⊗ B^{−}, (B^{+} −∘ A^{−}) × (B^{−} ∘− A^{+})) → (A^{+} ⊙ B^{−}, (B^{+} −^{•} A^{−}) × (B^{−} ^{•}− A^{+}))

which is a combination of the entropy ε_{A,B} and its left and right exponential variations, ε^{∗}, ε_{∗}.

So we have managed to get full entropic categories from intuitionistic entropic ones, but the reader is allowed to find that the construction above gives slightly degenerate results. In particular, the dualizing object is its own dual (it is the tensor unit as well, which says that the category interprets the mix rule). We now generalize this construction to more general dualizing objects.

3.8. Definition. Let C be a biautonomous category and ⊥ be an object in it. A bi-Chu object on ⊥ is a quadruple A = (A^{+}, A^{−}, l, r), where A^{+}, A^{−} are objects of C, l a morphism A^{+} ⊙ A^{−} → ⊥, and r a morphism A^{−} ⊙ A^{+} → ⊥. A morphism f: A → B is a pair f^{+} : A^{+} → B^{+}, f^{−}: B^{−} → A^{−} such that the following diagrams commute:

[figure: A^{+} ⊙ B^{−}; A^{+} ⊙ f^{−}; A^{+} ⊙ A^{−}; B^{+} ⊙ B^{−}; f^{+} ⊙ B^{−}; l_{B}; ⊥; l_{A}; B^{−} ⊙ A^{+}; f^{−} ⊙ A^{+}; A^{−} ⊙ A^{+}; B^{−} ⊙ B^{+}; B^{−} ⊙ f^{+}; r_{B}; ⊥; r_{A}]

If ⊥ is a cyclic object, a cyclic Chu object is a bi-Chu object of the form

A = (A^{+}, A^{−}, l, χ(l)).

So it takes a single morphism A^{+} ⊙ A^{−} → ⊥ to determine a cyclic Chu object, and it looks like an object in the ordinary Chu construction. The category of bi-Chu objects over ⊥ has its own tensor product which is constructed as follows: given A, B bi-Chu objects, then A ⊙ B is the quadruple (A^{+} ⊙ B^{+}, X, l, r), where X is obtained by the pullback

[figure: X; p; B^{−} ^{•}− A^{+}; B^{+} −^{•} A^{−}; q; g; B^{+} −^{•} ⊥^{•}− A^{+}; f]

the bottom horizontal map g is the double exponential transpose of

[figure: B^{+} ⊙ (B^{+} −^{•} A^{−}) ⊙ A^{+}; ev ⊙ A^{−}; A^{−} ⊙ A^{+}; r; ⊥]

and the right vertical map f the double exponential transpose of

[figure: B^{+} ⊙ (B^{−} ^{•}− A^{+}) ⊙ A^{+}; B^{+} ⊙ ev; B^{+} ⊙ B^{−}; l; ⊥ .]

The maps l_{A⊙B}, r_{A⊙B} associated to the tensor is are as follows. l is the composite:

[figure: A^{+} ⊙ B^{+} ⊙ X; A^{+} ⊙ B^{+} ⊙ q; A^{+} ⊙ B^{+} ⊙ (B^{+} −^{•} A^{−}); A^{−} ⊙ ev; A^{+} ⊙ A^{−}; l; ⊥]

while r is obtained by

[figure: X ⊙ A^{+} ⊙ B^{+}; p ⊙ A^{+} ⊙ B^{+}; (B^{−} ^{•}− A^{+}) ⊙ A^{+} ⊙ B^{+}; ev ⊙ B^{+}; B^{−} ⊙ B^{+}; r; ⊥ .]

So our aim is to prove, among other things, that the category of bi-Chu objects over ⊥, with the tensor defined as above, is a cyclic ∗-autonomous category, and that if ⊥ is cyclic, the full subcategory of cyclic Chu objects, with the induced tensor structure is also a cyclic ∗-autonomous category. This can be done by direct computation, but we will use a slightly circuitous route, inspired by [5], which introduces some amount of meaning to all the diagram chasing.

3.9. Proposition. Let ⊥ be a cyclic object and A, B be two cyclic Chu objects over ⊥. Then A ⊙ B as defined above is a cyclic Chu object.

Proof. Given A, B cyclic, so r_{A} = χ(l_{A}), r_{B} = χ(l_{B}). Look at the the following sequence of morphisms, calling them f_{1}, f_{2}, f_{3}, f_{4} in order of appearance, where X, p, etc., are defined just as above.

[figure: A^{+} ⊙ B^{+} ⊙ X; A^{+} ⊙ B^{+} ⊙ q; A^{+} ⊙ B^{+} ⊙ (B^{+} −^{•} A^{−}); A^{−} ⊙ ev; A^{+} ⊙ A^{−}; l; ⊥]
[figure: B^{+} ⊙ X ⊙ A^{+}; B^{+} ⊙ q ⊙ A^{+}; B^{+} ⊙ (B^{+} −^{•} A^{−}) ⊙ A^{+}; ev ⊙ A^{+}; A^{−} ⊙ A^{+}; χ(l); ⊥]
[figure: B^{+} ⊙ X ⊙ A^{+}; B^{+} ⊙ p ⊙ A^{+}; B^{+} ⊙ (B^{−} ^{•}− A^{+}) ⊙ A^{+}; B^{+} ⊙ ev; B^{+} ⊙ B^{−}; l; ⊥]
[figure: X ⊙ A^{+} ⊙ B^{+}; p ⊙ A^{+} ⊙ B^{+}; (B^{−} ^{•}− A^{+}) ⊙ A^{+} ⊙ B^{+}; ev ⊙ B^{+}; B^{+} ⊙ B^{−}; χ(l); ⊥]

We have that f_{2} = f_{3} because they are the exponential transposes of gq and fp respectively. Because of the naturality of χ we have f_{2} = χ_{A^{+},B^{+}⊙X}(f_{1}) and f_{4} = χ_{B,X⊙A^{+}}(f_{3}). By the defining property of cyclicity if follows from this that f_{4} = χ_{A^{+}⊙B^{+},X}(f_{1}), but f_{1} = l_{A⊙B} and f_{4} = r_{A⊙B} and this shows A ⊙ B is cyclic.

3.10. Proposition. Let K be an object of C. There is a unique ⊙-monoid structure on (1, K) in C × C^{op} for which the unit is “transparent” (e.g. the multiplication 1 ⊙ 1 → 1 is the unique map determined by the monoidal structure, the unit 1 → 1 is identity, etc.).

The reason is that the multiplication, being a map

(1 ⊙ 1, (1 −^{•} K) × (K ^{•}− 1)) ^{}(1, K),

is entirely defined by the choice of a map K → K × K, and the unit law of the monoid structure forces that morphism to be the diagonal.

We will call such monoids diagonal monoids and write K = (1, K), and so identify the object of C with the one in C × C^{op}.

3.11. Proposition. Let K = (1, K) be a diagonal monoid in C × C^{op} and A an object of the same category. Then a right module (action) A ⊙ K → A is entirely determined by a single map r: A^{−} ⊙ A^{+} → K and a left module K ⊙ A → A is determined by a single map l: A^{+} ⊗ A^{−} → K. Any such pair (l, r) determines a bimodule structure, in other words, the two actions commute:

[figure: K ⊙ A ⊙ K; l ⊙ K; A ⊙ K; K ⊙ A; K ⊙ r; l; A; r]

Proof. For instance, a right module structure A ⊙ K → A is defined by

(A^{+} ⊙ 1, (1 −^{•} A^{−}) × (K ^{•}− A^{+})) → (A^{+}, A^{−})

, which boils down to three maps A^{+} ⊙ 1 → A^{+}, A^{−} → 1 −^{•} A^{−} and A^{−} → K ^{•}− A^{+}, and the module laws force the first two of these to be identity, so the only map that matters is the third one, which is better seen as A^{−} ⊙ A^{+} → K. It is easy to show that any such map will obey the “diagonal action law”. By symmetry the same goes for left module structures, and a simple computation shows that a left and a right module structure on the same object always commute.

3.12. Proposition. Given a biautonomous category C and an object ⊥ of it, then the category of bi-Chu objects over ⊥ is equivalent to the category of ⊥-bimodules, for the diagonal monoid ⊥.

The proof is obvious. Naturally, if ⊥ is cyclic it should be clear what a cyclic ⊥-module is, and that it corresponds to a cyclic Chu object.

The point of these definitions is that they give us a much more manageable way to deal with the tensor of bi-Chu objects and their entropic relatives. Let ⊥ be an object of C, (A, r) a right ⊥-module and (B, l) a left ⊥-module, for the diagonal. Then the tensor A ⊙_{⊥} B is the object of C × C^{op} defined by the coequalizer

[figure: A ⊙ ⊥ ⊙ B; r ⊙ B; A ⊙ l; A ⊙ B; A ⊙_{⊥} B]

This unfolds as follows

[figure: A^{+} ⊙ 1 ⊙ B^{+}; A^{+} ⊙ B^{+}; A^{+} ⊙ B^{+}; A^{+} ⊙ B^{+}] (1 ⊙ B^{+} −^{•} A^{−}) × (B^{+} −^{•} ⊥^{•}− A^{+}) × (B^{−} ^{•}− A^{+} ⊙ 1)

(B^{+} −^{•} A^{−}) × (B^{−} ^{•}− A^{+}) [figure: ⟨Id, g⟩ × Id; Id × ⟨f, Id⟩]

X^{}

where X, f, g are just as in the definition of tensor of bi-Chu objects, and we have taken some notational liberties. It is easy to see that the right equalizer diagram gives the same result as the pullback that defines X in the bi-Chu tensor definition, with the equalizer map above corresponding to ⟨q, p⟩. It is also easy to see that if l: ⊥ ⊙ A → A is a left module structure on A, then the fact that tensoring preserves coequalizers, having a right adjoint, allows us to define a map ⊥ ⊙ A ⊙ B → A ⊙ B:

[figure: ⊥ ⊙ A ⊙ ⊥ ⊙ B; ⊥ ⊙ r ⊙ B; ⊥ ⊙ A ⊙ l; ⊥ ⊙ A ⊙ B; ⊥ ⊙ A ⊙_{⊥} B; A ⊙ ⊥ ⊙ B; l_{A} ⊙ ⊥ ⊙ B; r ⊙ B; A ⊙ l; A ⊙ B; l_{A} ⊙ B; A ⊙_{⊥} B; . . . . . . . . . . . . . . . .]

A computation shows that this map will coincide with l_{A⊙B} as defined above. Naturally the same argument will do if we tensor with ⊥ to the right, so we have a higher-level interpretation for the left and right maps needed to define the tensor of two bi-Chu objects. So we get a painless proof of some earlier claims:

3.13. Theorem. The ⊙ operation on bi-Chu objects over ⊥ is a bifunctor, obeys the associative laws, and it has the two required right adjoints −^{•} and ^{•}−. In other words the category of bi-Chu objects is bi-autonomous. In addition, the object (⊥, 1), with associated left and right actions given by the two monoidal maps ⊥ ⊙ 1 → ⊥ and 1 ⊙ ⊥ → ⊥, is cyclic dualizing. Furthermore, if ⊥ is a cyclic dualizing object, then the full subcategory of cyclic Chu objects over ⊥ is also cyclic ∗-autonomous.

The proof is done by using the general theory of bimodules,^{2} see for example [5]. Naturally everything can also be calculated by hand.

We can now consider the case where there are two tensor structures ⊗, ⊙, linked by a monoidal transformation ε: ⊗ → ⊙. At first the assumption that one of them is commutative has no importance. So, given a new tensor structure ⊗ on C, equipped with its left and right implications −∘ , ∘−, the notion of a ⊗-bi-Chu object on ⊥ (equivalently of a ⊗ − ⊥-bimodule in C × C^{op}) can de defined just as before. Naturally we get a different category, at the level of objects as well as morphisms. Given a right diagonal action r: A ⊗ ⊥ → A and a left action l: ⊥ ⊗ B → B we can construct a tensor object in C × C^{op}:

[figure: A ⊗ ⊥ ⊗ B; r ⊗ B; A ⊗ l; A ⊗ B; A ⊗_{⊥} B .]

Now suppose there is a monoidal ε: ⊗ → ⊙. It is easy to see that every left diagonal ⊙-action ⊥ ⊙ A → A can be turned into a left diagonal ⊗-action ⊥ ⊗ A → A by precomposition with ε. If things are seen from the Chu point of view, this is simply going from l: A^{+} ⊙ A^{−} → ⊥ to l ∘ ε: A^{+} ⊗ A^{−} → ⊥. Furthermore, given A, B ⊙-bimodules, not only is there an immediate definition of the object A ⊗_{⊥} B, using the induced ⊗ actions, but this object can be turned naturally into a ⊙-bimodule, e.g., the left action on A ⊗_{⊥} B being defined as

2Here we would like to make the distinction that for us bimodules are considered strictly as objects in a category, while some other researchers [27, 23] have connected linear logic with the use of bimodules as 1-cells in a higher-level categorical structure.

[figure: ⊥ ⊙ A ⊗ ⊥ ⊗ B; ⊥ ⊙ ε r ⊗ B; ⊥ ⊙ A ⊗ ε l; ⊥ ⊙ A ⊗ B; ⊥ ⊙ A ⊗_{⊥} B; A ⊗ ⊥ ⊗ B; l_{A} ⊗ ⊥ ⊗ B; ε r ⊗ B; A ⊗ ε l; A ⊗ B; l_{A} ⊗ B; A ⊗_{⊥} B; . . . . . . . . . . . . . . . .]

and the same going for the right action. Notice that the monoidality of ε is needed for the left squares to commute.

So we get

3.14. Theorem. If (C, ⊗, ⊙, ε) is as above, and ⊥ is any object in it, the category of ⊙-bi-Chu objects over ⊥ is equipped with an additional tensor operation ⊗_{⊥} which is a bifunctor, obeys the monoidal laws, is equipped with a monoidal map ⊗_{⊥} → ⊙_{⊥}, has both left and right implications as right adjoints, and has (⊥, 1) as dualizing object.

Proof. The proof uses the very same techniques as in the previous theorem. Let us unravel the constructions. Given A, B, X, p, q etc as in Definition 3.8, the object A ⊗_{⊥} B is the pair (A ⊗ B, X′) in C × C^{op}, with X′ the result of the pullback

[figure: X′; p′; B^{−} ∘− A^{+}; B^{+} −∘ A^{−}; q′; g′; B^{+} −∘ ⊥ ∘− A^{+}; f]

where g′ is the double exponential transpose of

[figure: B^{+} ⊗ (B^{+} −∘ A^{−}) ⊗ A^{+}; ev ⊗ A^{+}; A^{−} ⊗ A^{+}; ε; A^{−} ⊙ A^{+}; r; ⊥]

and the right vertical map f′ the double exponential transpose of

[figure: B^{+} ⊗ (B^{−} ∘− A^{+}) ⊗ A^{+}; B^{+} ⊗ ev; B^{+} ⊗ B^{−}; ε; B^{+} ⊙ B^{−}; l; ⊥ .]

The maps l_{A⊗B}, r_{A⊗B} associated to the tensor are as follows. l is the composite:

\begin{matrix}A^{+} ⊗ B^{+} ⊙ X′ & & & & ⊥ \\ A^{+} ⊗ B^{+} ⊙ (B^{+} −∘ A^{−}) & A^{+} ⊗ B^{+} ⊙ q′_{} & \overline{A^{+} ⊗ B^{+} ⊙ ε^{∗}_{}} & A^{+} ⊗ B^{+} ⊙ (B^{+} −^{•} A^{−}) & \overline{A^{+} ⊗ ev_{}} & A^{+} ⊙ A^{−} & ^{l } \end{matrix}

while r is obtained by

\begin{matrix}X′ ⊙ A^{+} ⊗ B^{+} & & & & ⊥ \\ (B^{−} ∘− A^{+}) ⊙ A^{+} ⊗ B^{+} & p′ ⊙ A^{+} ⊗ B^{+}_{} & \overline{ε_{∗} ⊙ A^{+} ⊗ B^{+}_{}} & (B^{−} ^{•}− A^{+}) ⊙ A^{+} ⊗ B^{+} & \overline{ev ⊙ B^{+}_{}} & B^{−} ⊙ B^{+} & ^{r } \end{matrix}

The entropy is a map (A^{+} ⊗ B^{+}, X′) ^{(ε,v)}^{}(A^{+} ⊙ B^{+}, X) where v: X → X′ is obtained by matching the two pullback squares that define X, X′ using the commutativity of

[figure: B^{+} −^{•} A^{−}; B^{+} −∘ A^{−}; B^{+} −^{•} ⊥^{•}− A^{+}; g; B^{+} −∘ ⊥ ∘− A^{+}; g′; B^{−} ^{•}− A^{+}; B^{−} ∘− A^{+}; B^{+} −^{•} ⊥^{•}− A^{+}; f; B^{+} −∘ ⊥ ∘− A^{+}; f′]

which should be obvious.

So we are left with considering what happens when one of the tensors is symmetric. Let this be the case for ⊗, so we are saying ε is an entropy.

3.15. Definition. Let C be an intuitionistic entropic category, and ⊥ an object. A ⊙- bi-Chu object A is said to be ⊗-compatible if the induced left and right ⊗-actions coincide, in other words if the following commutes:

[figure: A^{−} ⊗ A^{+}; c ∼; A^{+} ⊗ A^{−}; ε; A^{+} ⊙ A^{−}; A^{−} ⊙ A^{+}; ε; r; ⊥; l]

It should be obvious that if ⊥ is compatible with the symmetry, then every cyclic Chu object is ⊗-compatible.

3.16. Theorem. Let C be an intuitionistic entropic category and ⊥ an object. Then the full subcategory of bi-Chu objects over ⊥ that are ⊗-compatible, with the induced tensors and assorted structures, is an entropic category. If ⊥ is a cyclic object which is compatible with the symmetry, the category of cyclic Chu objects over ⊥ is an entropic category.

Proof. It suffices to show that the property of being ⊗-compatible is stable under the two tensors and the negation (it is obviously true for the unit and dualizer), and that the symmetry on the original ⊗ is carried to the category of bi-Chu objects.

Let now M = ℕ^{2} be the partial bimonoid we have constructed, and (U, ⊗, −∘) an autonomous category with sums. Let A, B ∈ U^{M}. By unfolding the definitions of ∘, ∗ we get, when m ≠ 0, n ≠ 0:

\begin{aligned}(A ⊗ B)_{(m,n)} & = & A_{(0,0)} ⊗ B_{(m,n)} & + & A_{(m,n)} ⊗ B_{(0,0)} \\ (A ⊙ B)_{(m,n)} & = & ∑_{0≤b≤n−1} A_{(0,b)} ⊗ B_{(m,n−b)} & + & ∑_{0≤a≤m−1} A_{(m−a,n)} ⊗ B_{(a,0)} & + A_{(0,n)} ⊗ B_{(m,0)} , \end{aligned}

when m ≠ 0:

\begin{aligned}(A ⊗ B)_{(m,0)} & = & ∑_{0≤a≤m−1} A_{(m−a,0)} ⊗ B_{(a,0)} \\ (A ⊙ B)_{(m,0)} & = & ∑_{0≤a≤m−1} A_{(m−a,0)} ⊗ B_{(a,0)} , \end{aligned}

and when n ≠ 0

\begin{aligned}(A ⊗ B)_{(0,n)} & = & ∑_{0≤b≤n−1} A_{(0,b)} ⊗ B_{(0,n−b)} \\ (A ⊙ B)_{(0,n)} & = & ∑_{0≤b≤n−1} A_{(0,b)} ⊗ B_{(0,n−b)} , \end{aligned}

and finally

\begin{aligned}(A ⊗ B)_{(0,0)} & = & A_{(0,0)} ⊗ B_{(0,0)} \\ (A ⊙ B)_{(0,0)} & = & A_{(0,0)} ⊗ B_{(0,0)} . \end{aligned}

For each of these two-line formulas, it should be obvious how the top line is embedded into the bottom line, and that the entropy is obtained by combining the four components. It should also be clear how the symmetry (A ⊗ B)_{(m,n)} ^{}(B ⊗ A)_{(m,n)} is defined. The reader can check what it means for a bi-⊙-Chu structure to be compatible with ⊗, which should now be pretty obvious.

In addition we have

3.17. Proposition. Let K ⊆ M be the set ({0} × ℕ) ∪ (ℕ × {0}). Any C ∈ U^{M} such that C_{m,m′} is the terminal object for all (m, m′) ∉ K is a cyclic object which is compatible with the symmetric tensor.

Proof. Given an element (m, m′) ∈ M we will abbreviate it as m̃. Assume that C has the property above. Choose any m̃ ∈ ℕ^{2} and B ∈ UM ; m̃. Since (M, ∘) has the cancellation law (whenever things are defined) we know that the set {(ñ, p̃) | m̃ ∘ p̃ = ñ} is equal to m̃ ∘ M = {m̃ ∘ p̃ | p̃ ∈ M}, and the same goes for {(ñ, p̃) | p̃ ∘ m̃ = ñ}, which can be written as M ∘ m̃. Thus we have

(C ∘− B)m̃ = ∏_{p̃∈M} Bp̃ −∘ C_{m̃∘p̃} and

(B −∘ C)m̃ = ∏_{p̃∈M} Bp̃ −∘ C_{p̃∘m̃} ,

and since m̃∘M ∩M ∘m̃ ⊆ K (exercise), the fact that C “is terminal outside of K” allows the construction of an iso (C ∘− B) ≅ (B −∘ C), which is obviously natural since nothing about B has been used. The computations for the tensors above show that the map

Hom(A ⊙ B, C) ^{Hom(ε,C)}^{}Hom(A ⊗ B, C)

induced by the entropy is actually an isomorphism: from this the cyclicity condition of C and the fact that it is compatible with the symmetry follows easily.

4. Entropic Hopf algebras

4.1. Hopf algebras and representations. In this section we give a quick summary of the necessary background in bialgebras and Hopf algebras. For suitable introductions, see [29, 1].

A Hopf algebra is a k-vector space, H, equipped with an algebra structure, a compatible coalgebra structure (= bialgebra) and an antipode satisfying the appropriate equations. Table 1 summarizes the necessary structure [29]. We say a Hopf algebra is (co)commutative if the (co)multiplication is (co)commutative, i.e., the appropriate diagram or its dual commutes. A basic example of (cocommutative) Hopf algebra is the group algebra k[G] of a group G, where the multiplication extends linearly the multiplication in G and the comultiplication extends linearly the codiagonal g ↦ g ⊗ g; k[G] is commutative if and only if G is abelian.

Structure  Equations
Algebra Multiplication μ: H ⊗ H → H Associativity
Unit η: k→H  η(1) 2-sided unit for μ
Coalgebra Comultiplication Δ: H → H ⊗ H  Coassociativity - Counit
Counit ϵ: H → k  (Dual equations)
Bialgebra Algebra + Coalgebra Δ and ϵ algebra homs

(equivalently μ, η coalgebra homs)

Hopf algebra Bialgebra + Antipode S: H → H Inverse to id_{H} under convolution

Table 1: Hopf algebras.

Given a Hopf algebra H, a module over H is a vector space V, equipped with a k-linear map called an H-action ρ: H ⊗ V →V such that evident diagrams commute. There is an evident notion of morphism of modules, i.e. linear maps satisfying f(hv) = hf(v) for all h ∈ H, v ∈ V. We thus obtain a category Mod(H).

We have the following result (see, for example, [25]).

4.2. Theorem. Mod(H) is a monoidal category. If the Hopf algebra is cocommutative, then the tensor product is symmetric. The unit for the tensor is given by the ground field with the module structure induced by the counit of H. If H has a bijective antipode, then Mod(H) is a biautonomous category. If H is commutative or cocommutative, then the antipode is involutive. In the case of a cocommutative Hopf algebra, the two internal homs are equal. The forgetful functor to the category of vector spaces is a monoidal closed functor.

The category TMod(H) is defined as follows. Objects are modules (V, ρ) such that V is equipped with a linear topology, and such that the action of H on V is continuous, for each element h ∈ H. Maps are H-maps which are also continuous. Define RTMod(H) to be the full subcategory of reflexive objects. The following results are presented in [6]. They are a straightforward generalization of the results of [25].

4.3. Theorem. Let H be a Hopf algebra with bijective antipode. Then RTMod(H) is a bi-∗-autonomous category. Furthermore, if H has an involutive antipode, i.e. S^{2} = id, then RTMod(H) is a cyclic ∗-autonomous category. If V is an H-module, the action on V^{∗} is given by hf(v) = f(S(h)v).

We also point out that there is an evident notion of comodule, and all of the above results dualize easily.

As should be clear from the above, representations of Hopf algebras provide a wide variety of examples of monoidal and monoidal closed categories. As such, it is also a rich setting to construct models of (multiplicative) linear logic. This was first suggested in [6], and demonstrated in [9] where a full completeness theorem for cyclic multiplicative linear logic was obtained using the shuffle Hopf algebra.

Thus it is a natural question as to whether one can model NL using Hopf algebras. The first thing that is evident is that one will need a new notion of Hopf algebra to be able to simultaneously model the two tensors. We will in fact introduce several such structures. We will have notions of entropic and coentropic Hopf algebras, and we will have both strong and weak notions of each.

4.4. Bigroups. Given that the prototypical example of a Hopf algebra is the vector space generated by a group, we introduce a modification of the notion of group appropriate for modeling NL.

4.5. Definition. A bigroup consists of a set X with the following additional structure:

X = (X, ∘, ∗, S_{1}, S_{2}, 1)

where ∘ and ∗ are multiplications on X with ∗ being commutative, S_{1} and S_{2} are endomorphisms of X and 1 is an element of X such that (X, ∘, S_{1}, 1) and (X, ∗, S_{2}, 1) are both groups (S_{i} acting as inverse). A bigroup is strong if furthermore S_{1} = S_{2}.

So a bigroup is a set with two group structures sharing the same unit element, and in the strong case, the same inverses.

4.6. Examples. Any abelian group is trivially a bigroup, taking both operations to be the same. A natural way of constructing bigroups is via the notion of semidirect product of groups (see, e.g., [19]). Let H and G be groups, and suppose θ: H→ Aut(G) is a group homomorphism. Define a multiplication on G × H by (g, h)(g′, h′) = (gθ(h)(g′), hh′). This makes G × H into a group with unit (e_{G}, e_{H}) and inverse given by (g, h)^{−1} = (θ(h^{−1})(g^{−1}), h^{−1}). This group structure is called the semidirect product and is denoted by G ⋊_{θ} H. Naturally there is another group structure on G × H, given by the direct product structure.

Thus semidirect products provide examples of (weak) bigroups, and hence, as we will see, models of NL. More generally there is the notion of bicrossed products of groups (see for example [19]), and these will similarly yield models. Indeed it seems quite possible that entropic categories will provide a natural setting for the examination of such twisted product structures.

A method of constructing strong bigroups is as follows. If X and Y are groups, find a bijective function f: X → Y which preserves unit and inverse but not the multiplication, and define a second multiplication on X by saying x ∗ x′ = f^{−1}(f(x)f(x′)): it is then straightforward to check that this induces a strong bigroup structure on X. For such a function f to exist, X and Y should obviously have the same cardinality, but it does not suffice: if X^{i} denotes the set of x ∈ X such that xx = 1 (the “involutions” of X), then, clearly, another necessary condition for the existence of such an f is that X^{i} and Y^{i} also have same cardinality, since x = x^{−1} is equivalent to f(x) = f(x^{−1}) = f(x)^{−1}. Now, conversely, these two conditions are sufficent: if X and Y have same cardinality and same number of involutions, write X \ X^{i} = X′_{1} ⊎ X′_{2} with the property that x ∈ X′_{1} if and only if x^{−1} ∈ X′_{2} (this is clearly possible and not unique), and analogously Y \ Y^{i} = Y′_{1} ⊎ Y′_{2}; then take a bijection f^{i}: X^{i} → Y^{i} such that f^{i}(1) = 1 and a bijection f′: X′_{1} → Y′_{1}, and define f: X → Y by:

\{ \begin{matrix}x ∈ X^{i} & ↦ & f(x) = f^{i}(x) ∈ Y^{i} \\ x ∈ X′_{1} & ↦ & f(x) = f′(x) ∈ Y′_{1} \\ x ∈ X′_{2} & ↦ & f(x) = f′(x^{−1})^{−1} ∈ Y′_{2}. \end{matrix}

Elementary concrete examples of this construction arise for instance by considering semidirect products of cyclic groups Z_{n} = Z/nZ. Take X = Z_{k} × Z_{n} and Y = Z_{k} ⋊ Z_{n}: if n and the Euler phi number ϕ(k) = ♯ Aut(Z_{k}) are not relatively prime, there is a nontrivial action of Z_{n} on Z_{k}, and if n is odd, X and Y obviously have the same number of involutions. If, e.g., k = p^{α} (Z_{k} a p-group), then ϕ(k) = p^{α−1}(p − 1) and we may take n = p or p − 1. If n is an odd prime and k = n^{2}, then ϕ(k) = n(n − 1), etc. Note in addition that in these examples, one multiplication is commutative and the other one is not, thus leading to the kind of structures we are seeking.

Let G be a set. Then the vector space spanned by G has a standard co-commutative coalgebra structure, generated by the diagonal G → G × G and the unique function G to the singleton. It is a standard result that if V is a comodule on that coalgebra, then V has a canonical decomposition of the form V = ⨁_{g∈G} V_{g}. The spaces V_{g} are called the homogeneous components of V. A typical element of V_{g} will be denoted v_{g}. Furthermore, a morphism of comodules f: V → W respects that decomposition, so not only do we have that f = ⨁_{g∈G} f_{g}, with f_{g}: V_{g} → W_{g}, but that any family (f_{g}: V_{g} → W_{g})_{g∈G} of linear maps determines a map of comodules V → W. Let now G be equipped with a group structure. The group Hopf algebra of G has that “diagonal” structure for its comultiplication, with its multiplication structure generated by the multiplication law on G. From this it follows that the tensor is given by setting (V ⊗ W)_{g} = ⨁_{g_{1}g_{2}=g} V_{g_{1}} ⊗ W_{g_{2}}. In other words, in the world of vector spaces, group and monoid bialgebras provide another way of presenting the construction of the tensor(s) in Theorem 3.4. We also note that if the group is finite, then this construction dualizes and there is a Hopf algebra structure on the dual space such that modules for this Hopf algebra are comodules for the original.

In the case of a strong bigroup, the resulting category of comodules will have two monoidal closed structures, or in the topological case, two ∗-autonomous structures. Furthermore, since one of the two group structures is abelian, one of the two monoidal structures will be symmetric. Since the antipode for such a Hopf algebra is involutive, we will also have that the negation is cyclic, as desired. (Since we have a strong bigroup, the negations coincide.) Thus we are extremely close to having an entropic category. We now explore the question of the existence of the entropy map. We assume for the rest of the section that we have a finite bigroup. We begin with the following definition.

4.7. Core of a bigroup. Let G be a bigroup. We will say that g ∈ G is in the core of G if g ∗ (−) = g ∘ (−) = (−) ∘ g. We denote the core of G by Core(G).

Thus a core element is one in which all the possible multiplications agree. We first have the following lemma.

4.8. Lemma.

• If g ∈ Core(G), then S_{1}(g) = S_{2}(g). Denote this element by g^{−1}. (Of course, in a strong bigroup, this is true of all elements.)

• If g, h ∈ Core(G), then gh ∈ Core(G).

• If g ∈ Core(G) and gh ∈ Core(G), then h ∈ Core(G).

• If g ∈ Core(G), then g^{−1} ∈ Core(G).

We now show that we indeed have an entropic category.

4.9. Theorem. Let G be a finite strong bigroup such that its ∗-multiplication is abelian. Denote the resulting symmetric tensor product by ⊗ and the second monoidal structure by ⊙. Construct a natural transformation T: A ⊗ B → A ⊙ B by the formula:

T (v_{g} ⊗ w_{g′}) = \{ \begin{matrix}v_{g} ⊗ w_{g′} & if g or g′ ∈ Core(G) \\ 0 & otherwise. \end{matrix}

Then the above construction defines an entropic category.

The above result is a straightforward exercise making use of the previous lemma to show that T is indeed a map of modules, satisfying the appropriate equations. This theorem not only gives us nontrivial examples of entropic categories, it suggests a general Hopf-algebraic approach to constructing many such categories. We begin by offering the following definition.

4.10. Definition (Entropic Hopf algebras).

• An entropic Hopf algebra consists of a vector space H, with an algebra structure (H, μ, η), two coalgebra structures (H, Δ_{1}, ϵ) and (H, Δ_{1}, ϵ), the first being cocommutative, and two antipodes S_{1} and S_{2}. (Note that the two counits coincide.) These must satisfy that (H, μ, η, Δ_{1}, ϵ, S_{1}) and (H, μ, η, Δ_{2}, ϵ, S_{2}) are both Hopf algebras. Furthermore, H must come equipped with an element Ψ = ΣΨ^{1} ⊗ Ψ^{2} ∈ H ⊗ H satisfying the following (where the subsript in Ψ_{1}^{2} and so on always refers to the first compultiplication.) Also note that Δ_{1}(h) = Σh_{1} ⊗ h_{2} and Δ_{2}(h) = Σ′h_{1} ⊗ h_{2}. For all h ∈ H:

ΣΨ^{1}h_{1} ⊗ Ψ^{2}h_{2} = Σ′h_{1}Ψ^{1} ⊗ h_{2}Ψ^{2}  (1)
Σϵ(Ψ^{2})Ψ^{1} = Σϵ(Ψ^{1})Ψ^{2} = 1_{H} = η(1)  (2)
ΣΨ^{1}Ψ_{1}^{1} ⊗ Ψ^{2}Ψ_{2}^{1} ⊗ Ψ^{2} = ΣΨ^{1} ⊗ Ψ^{1}Ψ_{1}^{2} ⊗ Ψ^{2}Ψ_{2}^{2}  (3)
Σf(Ψ^{1}a ⊗ Ψ^{2}b) = Σf(Ψ^{2}a ⊗ Ψ^{1}b)  (4)

In this final equation, f: A ⊙ B→k is an arbitrary map of H-modules.

• A strong entropic Hopf algebra is an entropic Hopf algebra such that S_{1} = S_{2}.

• A coentropic Hopf algebra is a vector space H with a coalgebra structure (H, Δ, ϵ), two algebra structures (H, μ_{1}, η) and (H, μ_{2}, η), and two antipodes S_{1} and S_{2}. H must also come equipped with a functional ρ: H ⊗ H→k called the entropic functional satisfying evident duals of the above equations. A strong coentropic Hopf algebra is a coentropic Hopf algebra such that S_{1} = S_{2}.

Some explanation is in order. In the entropic case, we will use the two comultipications to define two tensor products on the module category. Δ_{1} will supply the commutative conjunction ⊗ and Δ_{2} will supply the non-commutative conjunction ⊙. We will construct the entropy map ε: A ⊗ B→A ⊙ B via the formula:

ε(a ⊗ b) = ΣΨ^{1}a ⊗ Ψ^{2}b = Ψ(a ⊗ b).

Then, with this interpretation, Equation 1 says that the map ε is a morphism of Hmodules. Equations 2 and 3 say that the map is monoidal, and Equation 4 then implies that ⊥, which in our interpretation is the base field, is compatible with the symmetry.

The construction of the entropy map in the category of comodules for a coentropic Hopf algebra is dual to the above in an evident sense. We also note that as a consequence of the above definition, the antipode of a strong (co)entropic Hopf algebra is necessarily involutive.

Our previous discussion on bigroups provides a rich class of examples:

4.11. Theorem. If G is a bigroup, then k[G] is a coentropic Hopf algebra with the entropic functional given by ρ(g ⊗ g′) = 1 if g or g′ is in the core of G, and 0 otherwise. If G is also strong, then we get a strong coentropic Hopf algebra. If G is finite, the dual statements hold for k[G]^{∗}

Given the above construction, we can now state:

4.12. Theorem.

• If H is an entropic (resp. coentropic) Hopf algebra, then Mod(H) (resp. Comod(H)) is a symmetric monoidal closed entropic category.

• If H is a strong entropic (resp. coentropic) Hopf algebra, then RTMod(H) (resp. RTComod(H)) is an entropic category.

4.13. Matched pairs of Hopf algebras. One possible method of constructing (co)- entropic Hopf algebras is suggested by our previous observation concerning semidirect products of groups. We mention the following definition which has been examined extensively by Majid [25]. We will follow the presentation of Kassel, Chapter 9 [19].

A pair of Hopf algebras (X, A) is matched if there exist morphisms α: A ⊗ X → X and β: A ⊗ X → A making X into a left module-coalgebra over A and A a right modulecoalgebra over X. These maps must also satisfy a set of equations set out, for example, in [19] Definition 9.2.1.

One then has the following theorem. See [25] or [19], Theorem 9.2.3.

4.14. Theorem. Let (X, A) be a matched pair of Hopf algebras. Then there is a Hopf algebra structure on X ⊗ A described as follows. The coalgebra structure is the usual tensor coalgebra. The multiplication is given by:

(x ⊗ a)(y ⊗ b) = ∑ xα(a_{1} ⊗ y_{1}) ⊗ β(a_{2} ⊗ y_{2})b.

The unit for this algebra is 1 ⊗ 1, and there is also a formula for the antipode.

Thus a mixed pair of Hopf algebras produces two Hopf algebraic structures on X ⊗ A, one being the ordinary tensor product of Hopf algebras, and the other being the bicrossed product defined by the above theorem. The only remaining issue for producing a coentropic Hopf algebra is the existence of the entropy functional. We believe in fact that our notion of entropic category will provide an appropriate framework for the general analysis of such bicrossed products. But we leave this for a sequel.

5. Tannaka-Krein reconstruction for entropic Hopf algebras

It is by now quite well established that categories of representations of Hopf algebras provide fundamental examples of monoidal categories which have applications to many branches of mathematics. The significance of such categories is further strengthened by the importance of the various Tannaka-Krein theorems. We give a brief overview of the theory here, but see [25] for a much more extensive discussion.

In the original formulation, the Tannaka-Krein theorem concerned the representation theory of compact groups. In modern terminology, it can be viewed as a statement of how one can reconstruct a compact group from its category of representations. The subsequent generalization to commutative Hopf algebras was achieved by Saavedra-Rivano in [26] and further examined by Deligne and Milne in [13]. It was subsequently extended to the noncommutative setting by Ulbrich [30], and to the braided setting, where one obtains a quasitriangular structure, by Majid [24]. It is an extremely active area of research to this day, and is especially prevalent in the work of Majid [25].

For readers unfamiliar with these ideas, we begin with an overview following the presentation of [30] closely. One begins with a field k and C a k-linear, essentially small, abelian category. (For undefined terminology in this section, see [15] or [10].) One then also supposes that one has a functor U: C → k-Vec_{fd} which is k-linear, exact and faithful. Then Saavedra-Rivano [26] shows that there is a k-coalgebra A and an equivalence of categories E: C ≅ Comod_{fd}(A) such that U = EF where F: Comod_{fd}(A) → k-Vec_{fd} is the usual forgetful functor.

One obtains this coalgebra A by showing that there is a vector space A such that for any vector space V, the functor V ↦ Nat(U, U ⊗ V) is representable by A. Thus we have an isomorphism, natural in V, of the form:

θ_{V} : Hom_{Vec}(A, V) ≅ Nat(U, U ⊗ V).

Letting V = A and considering the identity on the left, one obtains a natural transformation a: U → U ⊗A on the right. By considering (a⊗id)a: U → U ⊗A⊗A on the right, we obtain a linear map Δ: A → A ⊗ A on the left. Similarly by considering the isomorphism U ≅ U ⊗ k, one obtains a map ε: A → k. Saavedra-Rivano’s result is that these maps not only give A the structure of a coalgebra, but induce the equivalence discussed above.

This coalgebra is fundamental to all further work on reconstruction. Saavedra-Rivano then goes on to show that if C is also symmetric compact closed, the compact structure agreeing with the linear structure of C, and if the functor F is a symmetric, compact closed functor, then A is a commutative Hopf algebra, and the equivalence E is furthermore an equivalence of symmetric compact closed categories.

To see how the algebra part of A is constructed, one notes that the isomorphism θ extends to an evident natural isomorphism

Hom(A ⊗ A, V) ≅ Nat(U ⊗ U, U ⊗ U ⊗ V).

We leave it as an exercise to see how one uses this to obtain the commutative algebra structure of A, making A a commutative bialgebra, and then ultimately a Hopf algebra.

Ulbrich’s key observation is that one retains the bialgebra structure even if the original category C was not symmetric. (Of course, the bialgebra will no longer be commutative.) Then the existence of the antipode follows from the compact closed structure of C. This is his Theorem 1 on page 255 of [30]. For a similar discussion, see Section 9.4 of [25].

5.1. Extension to the entropic setting. We now extend the above results to the entropic setting. While the result is straightforward, it sheds light on the structure of the entropy map. So we suppose that we have an entropic category C such that C is also k-linear, essentially small and abelian. We further suppose the existence of a functor U: C → k-Vec_{fd} which is k-linear, exact and faithful, and furthermore takes both of the compact closed structures of C to the usual compact closed structure of k-Vec_{fd}.

Thus, as in the previous argument, one sees that we obtain a k-vector space A, which naturally comes equipped with a coalgebra structure (Δ, ϵ). One applies the previous argument regarding the algebra structure of A to each of the two monoidal structures of C individually. Thus A obtains two multiplications, μ_{1} and μ_{2}. Since the unit objects for the two monoidal structures are the same, we see that the identities for the two multiplications are equal. One then applies Ulbrich’s theorem to the two compact closed structures and a priori obtains two antipodes, one for each bialgebra. However, since the two dual structures are equal, we see that the two antipodes must be equal as well.

Thus it remains to consider the entropy transformation ε: ⊗ →^{·} ⊙. Applying our functor U to the entropy transformation, we obtain the following:

U(ε): U(V ⊗ W) → U(V ⊙ W),

or equivalently,

U(ε): U(V) ⊗ U(W) → U(V) ⊗ U(W).

Thus the entropy map induces a natural transformation from U ⊗U to itself. Considering the isomorphism:

Hom(A ⊗ A, V) ≅ Nat(U ⊗ U, U ⊗ U ⊗ V)

instantiated at the base field (V = k), we see that the entropy map corresponds to a linear functional ε̂: A ⊗ A → k. This map ε̂ induces the entropy map (at the level of vector spaces) as follows:

V ⊗ W → A ⊗ V ⊗ A ⊗ W ≅ A ⊗ A ⊗ V ⊗ W → k ⊗ V ⊗ W ≅ V ⊗ W = V ⊙ W.

Of course, the last equality is only equality of vector spaces. This functional ε̂ must satisfy several properties. First, the above map must be a map of comodules. Then there are equations corresponding to the requirement that the map be monoidal. But these are precisely the properties in the definition of strong coentropic Hopf algebra. Thus, we have proved:

5.2. Theorem (Tannaka-Krein reconstruction for entropic categories). Let k be a field and C a k-linear, abelian, essentially small entropic category. Suppose that U: C → k-Vec_{fd} is a k-linear, exact, faithful, coentropic functor. Then there is a strong coentropic Hopf algebra H and an equivalence of categories E: C ≅ Comod_{fd}(H) such that U = F E, where F: Comod_{fd}(H) → k-Vec_{fd}.

6. Conclusion

In future work, we hope to examine models arising from deformation and quantization [14]. We hope to analyze work of Gerstenhaber, Giaquinto and Schack on deformations of Hopf algebras [16]. In particular, they have introduced the notion of a preferred deformation. This is a deformation of the original algebraic structure such that the comultiplication is altered, but the multiplication is fixed (or conversely). Clearly this would be an ideal setting for constructing entropic Hopf algebras. But even more than this, studying deformation theory leads one to categories which have a continuous family of monoidal structures as opposed to the two monoidal structures considered here. The logical significance of this is unclear but seems well worth exploring. Furthermore, the homological structures crucial to deformation theory may shed light on the relation between the commutative and the non-commutative connectives of NL.

We would also like to extend our version of the Tannaka-Krein theorem to the setting of Chu categories, since it seems that (co)entropic categories are much more prevalent than their strong counterparts. More generally, it seems time to extend these reconstruction theorems to the ∗-autonomous setting, and possibly also extend them away from the abelian setting as well.

Another area which is worthwhile exploring is that of co-entropy. We have seen above that semantics for co-entropy rules can be constructed, and the general result given in [21] shows that the (multiplicative) calculus obtained by taking NL and replacing entropy by co-entropy has cut-elimination. Naturally the theory of proof nets for such a calculus has to be developed; one incentive is linguistic applications, since the commutative tensor can be thought of as “unordered juxtaposition of words”, and the non-commutative one “ordered juxtaposition”, i.e., concatenation.

458  RICHARD F. BLUTE, FRANÇOIS LAMARCHE, PAUL RUET

A. Appendix: Sequent calculus for multiplicative NL

Identity

⊢ A^{⊥}, A

Cut rules

\begin{matrix}⊢ Γ[A] & ⊢ A^{⊥}, Δ \\ ⊢ Γ[Δ] \end{matrix}  \begin{aligned}⊢ Γ, A & ⊢ Δ[A^{⊥}] \\ & ⊢ Δ[Γ] \end{aligned}
\begin{matrix}⊢ Γ[A] & ⊢ Δ, A^{⊥} \\ ⊢ Γ[Δ] \end{matrix}  \begin{aligned}⊢ A, Γ & ⊢ Δ[A^{⊥}] \\ & ⊢ Δ[Γ] \end{aligned}
\begin{matrix}⊢ Γ[A] & ⊢ A^{⊥}; Δ \\ ⊢ Γ[Δ] \end{matrix}  \begin{aligned}⊢ Γ; A & ⊢ Δ[A^{⊥}] \\ & ⊢ Δ[Γ] \end{aligned}
\begin{matrix}⊢ Γ[A] & ⊢ Δ; A^{⊥} \\ ⊢ Γ[Δ] \end{matrix}  \begin{aligned}⊢ A; Γ & ⊢ Δ[A^{⊥}] \\ & ⊢ Δ[Γ] \end{aligned}

Associativity - Commutativity

⊢ Π[Γ; (Δ; Σ)]

a1

⊢ Π[(Γ; Δ); Σ]

⊢ Π[(Γ; Δ); Σ]

1a

⊢ Π[Γ; (Δ; Σ)]

⊢ Π[Γ, (Δ, Σ)]

a2

⊢ Π[(Γ, Δ), Σ]

⊢ Π[(Γ, Δ), Σ]

2a

⊢ Π[Γ, (Δ, Σ)]

⊢ Π[Γ, Δ] ; com ; ⊢ Π[Δ, Γ]

Structural rules

⊢ (Γ; Δ); Σ ; entropy ; ⊢ (Γ, Δ), Σ  ⊢ Γ, Δ ; seesaw ; ⊢ Γ; Δ  ⊢ Γ; Δ ; coseesaw ; ⊢ Γ, Δ

Multiplicative rules

\begin{aligned}⊢ Γ; A & ⊢ Δ; B \\ & ⊙ \\ ⊢ (Δ; Γ); A ⊙ B \end{aligned}  \begin{aligned}⊢ Γ, A & ⊢ Δ, B \\ & ⊗ \\ ⊢ (Δ, Γ), A ⊗ B \end{aligned}  ⊢ 1
⊢ Γ; (A; B) ; ▽ ; ⊢ Γ; A ▽ B  ⊢ Γ, (A, B) ; ⅋ ; ⊢ Γ, A ⅋ B  \begin{aligned}⊢ Γ \\ & ⊥ \\ ⊢ Γ, ⊥ \end{aligned}

ENTROPIC HOPF ALGEBRAS AND MODELS OF NON-COMMUTATIVE LOGIC 459

References

[1] E. Abe. Hopf algebras. Cambridge University Press, 1980.

[2] V. M. Abrusci and P. Ruet. Non-commutative logic I: the multiplicative fragment. Annals Pure Appl. Logic, 101(1):29–64, 2000.

[3] M. Barr. ∗-autonomous categories. Springer LNM, 752, 1979.

[4] M. Barr. Non-symmetric ∗-autonomous categories. Theoret. Comp. Sci., 139:115– 130, 1995.

[5] M. Barr. The Chu construction. Theory Appl. Cat., 2:17–35, 1996.

[6] R. Blute. Hopf algebras and linear logic. Math. Struct. in Comp. Sci., 6:189–217, 1996.

[7] R. Blute, R. Cockett, and R. Seely. The logic of linear functors. To appear in Math. Struct. in Comp. Sci., 2002.

[8] R. Blute and P. J. Scott. Linear Läuchli semantics. Annals Pure Appl. Logic, 77:101– 142, 1996.

[9] R. Blute and P. J. Scott. The shuffle Hopf algebra and noncommutative full completeness. J. Symb. Logic, 63 (4):1413–1436, 1998.

[10] H. Cartan and S. Eilenberg. Homological Algebra. Princeton University Press, 1956.

[11] J. R. B. Cockett, J. Koslowski, and R. A. G. Seely. Introduction to linear bicategories. Math. Struct. in Comp. Sci., 10(2), 2000.

[12] B. J. Day. On closed categories of functors. In S. MacLane, editor, Reports of the Midwest Category Seminar. Springer LNM 137, 1970.

[13] P. Deligne and J. Milne. Tannakian categories. Springer LNM, 900:101–228, 1982.

[14] T. F. Fox. An introduction to algebraic deformation theory. J. Pure Appl. Algebra, 84, 1993.

[15] P. Freyd. Abelian Categories. Harper and Row, 1964.

[16] M. Gerstenhaber and S. D. Schack. Algebraic cohomology and deformation theory. In: Deformation Theory of Algebras and Structures and Applications, pages 11–264, 1988.

[17] J.-Y. Girard. Linear logic. Theoret. Comp. Sci., 50(1):1–102, 1987.

[18] A. Joyal. Une théorie combinatoire des séries formelles. Adv. Math., 42:1–82, 1981.

[19] Ch. Kassel. Quantum groups. Graduate Texts in Mathematics 155. Springer, 1995.

[20] G. M. Kelly and M. L. Laplaza. Coherence for compact closed categories. J. Pure Appl. Algebra, 19:193–213, 1980.

[21] F. Lamarche. On the algebra of structural contexts. Submitted, 2002. Available at

    http://www.loria.fr/˜ lamarche.

[22] J. Lambek. The mathematics of sentence structure. Amer. Math. Monthly, 65(3):154– 170, 1958.

[23] J. Lambek. Bilinear logic in algebra and linguistics. In J.Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, volume 222 of London Math. Soc. Lec. Notes, page 43. Cambridge University Press, 1994.

[24] S. Majid. Quasitriangular Hopf algebras and Yang-Baxter equations. Int. J. of Modern Physics, 5:1–91, 1990.

[25] S. Majid. Foundations of quantum group theory. Cambridge University Press, 1995.

[26] N. Saavedra Rivano. Catégories tannakiennes. Springer Lecture Notes in Mathematics, 265, 1972.

[27] K. Rosenthal. ∗-autonomous categories of bimodules. J. Pure and App. Algebra, 97(2):189–202, 1994.

[28] P. Ruet. Non-commutative logic II: sequent calculus and phase semantics. Math. Struct. in Comp. Sci., 10(2):277–312, 2000.

[29] M. Sweedler. Hopf algebras. W. A. Benjamin, 1969.

[30] K.H. Ulbrich. On Hopf algebras and rigid monoidal categories. Israel J. of Math., 72:252–256, 1990.

[31] D.N. Yetter. Quantales and (non-commutative) linear logic. J. Symb. Logic, 55(1), 1990.

University of Ottawa, Département de Mathématiques et Statistique, 585 avenue King Edward, Ottawa, Ontario K1N 6N5, Canada

INRIA-Lorraine & LORIA, Campus scientifique B.P. 239, 54506 Vandœuvre-lès-Nancy Cedex, France

CNRS - Institut de Mathématiques de Luminy, 163 avenue de Luminy, Case 907, 13288 Marseille Cedex 9, France

Email: rblute@mathstat.uottawa.ca
      lamarche@loria.fr
      ruet@iml.univ-mrs.fr

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/10/17/10-17.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh,

rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

Editorial board.

John Baez, University of California, Riverside: baez@math.ucr.edu Michael Barr, McGill University: barr@barrs.org, Associate Managing Editor Lawrence Breen, Université Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Palo Alto Research Center: paiva@parc.xerox.com Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Sydney: stevel@maths.usyd.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca, Managing Editor Jiri Rosicky, Masaryk University: rosicky@math.muni.cz James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca