Categories for computation in context and unified logic

R.F. Blute^{1}  J.R.B. Cockett^{2}  R.A.G. Seely^{3}

Presented to Peter Freyd to mark the occasion of his 60^{th} birthday

Abstract

In this paper we introduce context categories to provide a framework for computations in context. The structure also provides a basis for developing the categorical proof theory of Girard’s unified logic. A key feature of this logic is the separation of sequents into classical and linear zones. These zones may be modelled categorically as a context/computation separation given by a fibration. The perspective leads to an analysis of the exponential structure of linear logic using strength (or context) as the primitive notion.

Context is represented by the classical zone on the left of the turnstile in unified logic. To model the classical zone to the right of the turnstile, it is necessary to introduce a notion of cocontext. This results in a fibrational fork over context and cocontext and leads to the notion of a bicontext category. When we add the structure of a weakly distributive category in a suitably fork fibred manner, we obtain a model for a core fragment of unified logic.

We describe the sequent calculus for the fragment of unified logic modelled by context categories; cut elimination holds for this fragment. Categorical cut elimination also is valid, but a proof of this fact is deferred to a sequel.

Introduction

This document has its roots in the attempt to elucidate the structure of linear logic using weakly distributive categories [CS91]. In that programme we started by investigating the categorical proof theory of the (two-sided) linear cut rules, giving rise to the notion of weakly distributive categories. Our rationale was that by so doing we could better modularize the structure of linear logic which would facilitate the establishment of coherence theorems [BCST]. It was a natural step to ask whether the exponentials, ! and ? , could be added in a modular fashion to this basic setting [BCS92]. When we started to study this question, we were struck by the prominent role of tensorial strength (and costrength) in the formulation. This led us to consider whether it might be possible to use strength as a more primitive notion in the modular decomposition of these settings and resulted in the development of context categories^{1}.

1Department of Mathematics, University of Ottawa, 585 King Edward St., Ottawa, ON, K1N 6N5, Canada.

rblute@mathstat.uottawa.ca Research partially supported by Le Fonds FCAR, Québec, and NSERC, Canada.

2Department of Computer Science, University of Calgary, 2500 University Drive, Calgary, AL, T2N 1N4, Canada.

robin@cpsc.ucalgary.ca Research partially supported by NSERC, Canada.

3Department of Mathematics, McGill University, 805 Sherbrooke St., Montréal, PQ, H3A 2K6, Canada.

rags@math.mcgill.ca Research partially supported by Le Fonds FCAR, Québec, and NSERC, Canada.

The coherence conditions (over twenty commuting diagrams just for the notion of context) for a setting in which strength is taken as primitive are quite daunting. Indeed, initially, as we lacked any motivating models, we were concerned that these “context categories” would simply foist a needless and rather complex abstraction on the community. However, two connections persuaded us that this basic setting was worthwhile.

The first connection, which we explore in this paper, is the similarity of the system to Girard’s approach to amalgamating classical and linear logic into one setting. In a linear sequent calculus it is natural to model context by dividing the terms to the left of the turnstile into a “classical” portion followed by a “linear” portion. Context categories are the categorical proof theory of this fragment of Girard’s “unified logic” [G93]. Many of the significant features of the semantics of unified logic may be studied in this fragment alone, and although we press on to a more symmetric system, we suggest some attention is warranted for this more modest fragment. Indeed, it does provide the basic building block of the categorical proof theory for unified logic: by adding a cocontext one can then model the division of the terms to the right of the turnstile into a classical and linear portion. This allows one to view the linear portion as being fork fibred^{2} over the context and cocontext. To obtain the further “features” of linear logic we claim that one simply now adds them in a suitably fork fibred manner.

The second connection, which we do not explicitly explore in this paper but rather leave to future work, is to the “Action Calculi” of Robin Milner. Strength is of course a pervasive notion in computer science. The view of a function (or program) as a map between two objects in a given context is absolutely fundamental to computing. The categorical machinery for handling context in this sense is, specifically, strength and, in generality, fibration. That the former gives rise to the latter in the classical setting is known (this is detailed in [C91]). However, less well-explored is the notion of strength as applied to linear settings and this becomes quite important when reasoning about communicating processes. The fact that some processes are limited-resource or “threaded” leads naturally to treating them in a linear fashion. It was partly to accommodate these features that Milner developed his “Action Calculi” [M93]. These (or at least the static portion) provide another source of examples for context categories and contextual modules. For related work see [PR96] and [P96].

The development actually starts by describing the general notion of strength and how it gives rise to a fibration. The aim is to remind the reader of the correspondence that the various notions of strong functor, strong natural transformation etc. have to their fibrational counterparts. Formally, there is a full 2–embedding of these strong categories into (structured) fibrations. We briefly discuss datatypes and the properties one should expect of them in the presence of context.

Next we study context categories: these are categories with a natural contextual self-action. Much of the discussion is centered on the necessary but rather mundane task of establishing the coherence conditions both for context categories and for their actions (which we call contextual modules). We consider context categories both with and without the empty context ⊤: when the empty context is omitted there are a number of natural models. Its inclusion demands considerably more of the situation. In particular, empty context induces a “storage” cotriple which turns an object X into a context for ⊤: X ↦ X ⊘ ⊤. This is the contextual version of the ! operator of linear logic.

1We must point out that the similar term “contextual categories” has been used in a completely different sense by J. Cartmell [C86]. We use “context categories” to avoid a terminological clash, but shall use “contextual” as the corresponding adjective elsewhere.

2Here by being “fork fibred” we mean that there is a fibrational fork, i.e. a fibration over C^{op} × D. In this paper, we shall primarily be concerned with the case when C and D are actually the same categories; generally C is the context while D is the cocontext.

The structure so far is just half the basic story: with this we can account for contexts “on the left of the turnstile” (i.e. in the hypothesis). Our next step is therefore to address the remaining half: we dualize the material above, giving a notion of cocontext. For context and cocontext to fit together properly, there are three “weak distributivities” (very much in the spirit of [CS91]) which allow the construction of a fibrational fork from the fibration and cofibration induced by context and cocontext. These distributivities we will discover correspond precisely to the cut rules of the sequent calculus for unified logic.

To be able to handle at least the tensor-par fragment of linear logic, we must add these connectives as well. As mentioned above the strategy is to add these features in a bistrong manner. The interaction between the classical and linear portions of sequents then begins to develop some of the complexity we expect from linear logic.

Finally, we describe the fragment of unified logic, called the context calculus, for which these context categories are the proof theory. The categorical coherence diagrams may be seen as arising from those manipulations which are necessary to establish the cut elimination theorem. In a sequel to this paper we intend to describe the proof circuits for this logic. These provide a usable and more economical view of the whole calculus, and give a convenient description of the free structures for this doctrine. Rather than overwhelm the reader with the extremely long and opaque diagram chasing involved in establishing the theorems of the later sections—some of the diagrams involve at least thirty cells, which certainly overreaches our LaTEX formatting ability—we give an overview of the main results which we hope to present in a more transparent and complete style in a sequel which introduces the circuits.

To conclude, we would like to emphasize again the philosophy which underlies this work. In the series of papers of which this is a part we have repeatedly stressed the importance of tensorial strength in Girard’s logical systems. In this paper, for the first time, we take strength as our starting point and show how the categorical proof theory of Girard’s systems can be reconstructed. This manner of developing the proof theory gives, in particular, a very natural explanation of the exponentials and of the coherence conditions governing them. We would argue that hitherto such an explanation has been absent.

From this perspective, the original work on multiplicative linear logic did not pay sufficient attention to strength. In the case of unified logic the separation into classical and linear parts was suggestive of strength. However, the lack of connectives for the semicolons blocked any direct expression of the sense in which strength arose. While, in a sense, the crux in making the role of strength explicit is the simple technical expedient of introducing connectives (and the corresponding rules) to represent the semicolons, this belies its significance. The perspective provided by strength not only reveals a uniformity behind the details of the categorical proof theory, which hitherto was absent, but also provides a key to the proper understanding of the semantics of these settings.

1 Strength and fibrations

This section starts by introducing the notion of strength through the notion of a functorial action. Next structural actions are described. It is then shown that these can alternatively be formulated as a fibration.

Throughout this development we shall talk about “computations in context.” This terminology is not meant to prejudice the generality of the theory but rather to lend a certain intuition to the proceedings.

1.1 Functorial actions and strength Let X be a category then X is said to have an action on a category Y if there is a functor

⊘: X × Y ⟶ Y

A strong functor F: Y ⟶ Y′ between two categories with an X–action is a functor together with a natural transformation

θ: X ⊘ F (Y) ⟶ F (X ⊘ Y)

called a strength. A strong natural transformation between strong functors is an ordinary natural transformation α: F_{1} ⟶ F_{2} which satisfies the additional property:

[figure: X ⊘F_{1}(Y); 1⊘α; X ⊘F_{2}(Y); θ_{1}; θ_{2}; F_{1}(X ⊘Y); α; F_{2}(X ⊘Y)]

We shall often call these strong transformations. It is almost a formality to observe that: Proposition 1.1 Categories with an X–action, strong functors, and strong natural transformations form a 2–category Act(X).

The only ingredient in this which needs a comment is the manner of composing the strengths of strong functors:

(F, θ_{F}) ∘ (G, θ_{G}) = (F ∘ G, θ_{G}; G(θ_{F})).

1.2 Structural actions An action ⊘ is structural if the functor X ⊘ is a cotriple for each object X; explicitly this means that there are in addition the following natural transformations, called duplication and elimination:

d: X ⊘ Y ⟶ X ⊘ (X ⊘ Y)
e: X ⊘ Y ⟶ Y

where these data satisfy:

[figure: X ⊘ Y; e; X ⊘ (X ⊘ Y); 1⊘e; X ⊘ Y; d; X ⊘ Y]

[figure: X ⊘ Y; d; X ⊘ (X ⊘ Y); d; d; X ⊘ (X ⊘ Y); 1⊘d; X ⊘ (X ⊘ (X ⊘ Y))]

or equationally:

d; e = 1  (1)
d; 1 ⊘ e = 1  (2)
d; d = d; 1 ⊘ d  (3)

There is a standard structural action on any category Y. Let CoTriple(Y) be the category whose objects are cotriples (D, δ, ϵ) on Y and whose morphisms are cotriple homomorphisms. We may define a structural action:

⊘ : CoTriple(Y) × Y ⟶ Y

with T ⊘ Y = T (Y); the cotriple structure then gives the duplication and elimination map.

It is now obvious that: Lemma 1.2 There is a bijective correspondence between structural actions G: X × Y ⟶ Y and functors G′: X ⟶ CoTriple(Y) satisfying G(X, Y) = G′(X) ⊘ Y , d = δ_{G′(X)}: G′(X) ⊘ Y ⟶ G′(X) ⊘ (G′(X) ⊘ Y) and e = ϵ_{G′(X)}: G′(X) ⊘ Y ⟶ Y.

If Y is a monoidal category we say that a structural action is a monoidal structural action in case there is a functor F: X ⟶ Y such that X⊘Y = F (X)⊗Y and there are natural transformations Δ: F (X) ⟶ F (X)⊗F (X) and ι: F (X) ⟶ ⊤ satisfying the usual requirements for being a comonoid. Explicitly these are:

Δ; 1 ⊗ ι; uR_{⊗} = 1 = Δ; ι ⊗ 1; uL_{⊗}

Δ; Δ ⊗ 1; a_{⊗} = Δ; 1 ⊗ Δ.

We say it is a commutative monoidal structural action in case Y is a symmetric monoidal category and

Δ; c_{⊗} = Δ.

Any F with such a comonoid structure does give rise to a structural action: Lemma 1.3 If F: X ⟶ Y is a comonoid (as above) then ⊘ : X × Y ⟶ Y defined by (X, Y) ↦ F (X) ⊗ Y is a structural action with:

d = Δ ⊗ 1; a_{⊗}: X ⊘ Y ⟶ X ⊘ (X ⊘ Y)

e = ι ⊗ 1; uR_{⊗}: X ⊘ Y ⟶ Y.

As for general structural actions there is a standard monoidal action. Let CoMon(Y) be the category of comonoids and comonoid homomorphisms in Y; then the underlying functor U: CoMon(Y) ⟶ Y is immediately a monoidal structural action. Furthermore: Lemma 1.4 There is a bijective correspondence between monoidal structural actions given by F: X ⟶ Y and functors F′: X ⟶ CoMon(Y) satisfying F′; U = F, Δ_{F} = F′; Δ_{U}, and ι_{F} = F′; ι_{U}.

These ideas are closely related to the treatment of names in the action calculi, as analyzed by Pavlović [P96]. There he shows that to add an indeterminate to a symmetric monoidal category in a manner which is functionally complete (in the sense of Lambek and Scott [LS86]) is equivalent to moving to the Kleisli category induced by a commutative comonoid. He then uses this to explain the treatment of names in the static part of the action calculus. Thus, a commutative monoidal structural action provides a means to add functionally complete indeterminates at all acting types.

As mentioned in the introduction a motivating example is the “bang” functor of a MELL category: that is a category modelling the tensor and exponential fragment of linear logic described by Bierman in [B95]. The bang functor gives a monoidal structural self-action on any MELL category: we shall refer to such an action as a bang action. The action, then, is defined by X ⊘Y = ! X ⊗Y, and d and e are given by the following canonical maps.

d = ! X ⊗ Y ⟶ ( ! X ⊗ ! X) ⊗ Y ⟶ ! X ⊗ ( ! X ⊗ Y)
e = ! X ⊗ Y ⟶ ⊤ ⊗ Y ⟶ Y

Of particular relevance to this paper is the analysis of this situation provided by Nick Benton [Be94]: already implicit in his work was the use of bang as a structural action.

In the case that Y is a cartesian category, so that the tensor is the product, each object is a (commutative) comonoid in exactly one way. Thus, the standard monoidal action is simply × : Y × Y ⟶ Y and we call this the standard simple action of Y. The monoidal structural actions of a cartesian category Y are thus induced by arbitrary functors F: X ⟶ Y and we call these simple actions.

Next we extend the definitions of strong functors and transformations to the structural case. In fact, the strong transformations are unchanged from above, but structurally strong functors must also preserve the duplication and elimination structure. Specifically this means that the following diagrams must commute:

Elimination strength:

[figure: X ⊘ F (Y); θ; F (X ⊘ Y); e; F (e); F (Y)]

Duplication strength:

[figure: X ⊘ F (Y); d; X ⊘ (X ⊘ F (Y)); θ; 1 ⊘ θ; θ; F (X ⊘ Y); F (d); F (X ⊘ (X ⊘ Y))]

Once again it is a formality to show that Proposition 1.5 Categories with an X–structural action, structurally strong functors, and strong natural transformations form a 2–category StrAct(X), which is a sub-2–category of Act(X).

1.3 Fibrations and structural actions We suppose the reader is familiar with the basic notions concerning fibrations and indexed categories. See for example [Bo94].

An X–structural action on Y gives rise to an indexed category over X and thus a fibration over X. The fiber over an object X is to be thought of as the Y–computations in the context X. Thus, maps in the fiber are f: X ⊘ Y ⟶ Y′ and g: X ⊘ Y′ ⟶ Y′′ with composition given by d; 1⊘f; g: X ⊘Y ⟶ Y′′ and identities given by e: X ⊘Y ⟶ Y. This is of course the Kleisli category of the cotriple X ⊘ . Functors between these categories of computations in context are provided by precomposing with the change in context. The functorial nature of this change in context follows immediately from the naturality of the duplication and the elimination transformations.

Alternatively we may form the total category C_{X}(Y) of computations and contexts and show that the functor to X is a fibration. The objects of the total category are (following the Grothendieck construction) pairs (X, Y) where X ∈ X and Y ∈ Y, the maps are pairs (h, f): (X, Y) ⟶ (X′, Y′) where h: X ⟶ X′ and f: X ⊘ Y ⟶ Y′ is a computation in the context X.

Slightly more surprising is the fact that strong functors give rise to morphisms of fibrations and strong transformations to transformations of fibrations. The passage between the two is as follows:

• Strong functor to morphism of fibration: Given a strong functor F: Y ⟶ Y′ we may define a family of functors between Y–computations in context X and Y′–computations in context X. Let f: X ⊘ Y ⟶ Y′ then define F_{X}(f): X ⊘ F (Y) ⟶ F (Y′) to be

X ⊘ F (Y) ⟶^{θ} F (X ⊘ Y) ⟶^{F (f)} F (Y′).

It is straightforward to check that these are functors and they commute with the functors which change context.

• Strong transformation to fibrational transformation: Given a strong transformation α: F ⟶ G we have a transformation α_{X}: F_{X} ⟶ G_{X} defined in the obvious way by e; α: X ⊘ F (Y) ⟶ G(Y).

It is clear that this gives a faithful 2-functor from the 2–category StrAct(X) to the 2–category of fibrations over X. Our aim is now to supply a full and faithful 2–functor to a 2–category which we know to have all weighted limits. (We shall see in the next section that StrAct(X) does not have this property.) In order to achieve this we construct the comma 2–category between the following 2–functor and the identity:

Const: Cat ⟶ Fib(X) given by Y ↦ [Pr_{1}: Y × X ⟶ X].

An object of this 2–category ConstFib(X) is a triplet (Y, M: Pr_{1} ⟶ F, F), where F is a fibration over X and M is a morphism of fibrations from the constant fibration at Y. Theorem 1.6 For any category X there is a full and faithful 2–embedding V: StrAct(X) ⟶ ConstFib(X).

First we note that the functor K: Y × X ⟶ C_{X}(Y) sending (f, x) ↦ (e; f, x), which is the identity on objects but sends maps to those which do not use context is a morphism of fibrations. This is a 2–functorial assignment. We must show that it is full and faithful. To this end we show how from morphisms of fibrations and transformations of fibrations we can recapture their strong counterparts:

• Morphism of fibrations to strong functor: Given a 1–cell in ConstFib(X) between morphisms of fibrations given by structural actions, part of this data is a functor F: Y ⟶ Y′. It suffices to show that this is a strong functor. The strength at X for this functor is provided by the identity map on X ⊘ Y as seen in the fiber over X. Here the map 1: X ⊘ Y ⟶ X ⊘ Y is not the identity in the fibre over X, but is a map Y ⟶ X ⊘ Y, so under F turns into a map θ: X ⊘ F (Y) ⟶ F (X ⊘ Y), giving the required strength of F.

• Fibrational transformation to strong transformation: A transformation in ConstFib(X) has as part of its data an ordinary transformation. It suffices to show that it is strong which is a consequence of the fact that the transformation of the total category is natural at the particular maps which provide the strength.

1.4 2–limits and datatypes Given two X–structural actions Y and Y′ their product is an X–structural action given by:

X ⊘ (Y, Y′) = (X ⊘ Y, X ⊘ Y′).

Thus the 2–category of StrAct(X) has finite products.

Also StrAct(X) has “arrow” categories Y^{→}. This is the ordinary category of arrows with the

tensor action X ⊘ (Y ⟶^{f} Y′) = X ⊘ Y ⟶^{1 ⊘ f} X ⊘ Y′. The strength natural transformation for a functor into this arrow category gives a commutative square which expresses the strength of the natural transformation.

StrAct(X) does not have equalizers. If H is the equalizing functor of two functors of this 2– category F, G: Y ⟶ Y′ then certainly H ∘ F = H ∘ G as functors. However, taking the equalizer as mere functors will not do as this equalizer category need not be closed under the X–action.

Not only must H equalize the functors but also the composite must agree on the strengths and it is possible that H have a non-trivial strength (consider the pullback of the identity functor with an arbitrary functor expressed as an equalizer). This means that the equation

θ_{F}; F (θ_{H}) = θ_{G}; G(θ_{H})

must hold. This does not hold in general with a structural action.

Thus, the 2–category of StrAct(X) does not have all weighted limits.

By contrast, of course, the 2–category of fibrations (with morphisms preserving cleavage) certainly has equalizers and preserves the products and arrow categories of structural actions under the embedding. This is also true of the underlying functor to Cat. This means the full 2-embedding to ConstFib(X) preserves these limits. This allows us to regard this 2–category as a “completion” of the latter in which equalizers exist.

For the discussion of datatypes, inserters are needed [C91] and so it is pragmatic to work in the 2–category ConstFib(X) to determine the form datatypes take in this setting. When one unwinds the various diagrams involved for a structural action, the universal diagram which must be satisfied by a linear natural number object, for example, takes the following form:

[figure: X ⊘ 1; 1 ⊘ 0; X ⊘ N; 1 ⊘ s; X ⊘ N; f; λ; d; 1 ⊘ λ; C; g; X ⊘ C]

Note how it differs from the form suggested by Paré and Román [PR89] as the context appears not only on the top line but also on the bottom where the properties of being a context become crucial.

Perhaps the most important single inductive datatype is the list datatype. To construct lists a strong tensor product in Y is needed: the universal diagram for lists will then be:

[figure: X ⊘ ⊤; 1 ⊘ nil; X ⊘ list(A); 1 ⊘ cons; X ⊘ (A ⊗ list(A)); f; k; d; 1 ⊘ (θ_{A⊗} ; 1 ⊗ k); C; g; X ⊘ (A ⊗ C)]

Similarly one may define diagrams for other inductive datatypes. As datatypes have hardly been studied in these settings it would be interesting to know what properties they satisfy.

2 Context Categories

A situation of particular interest arises when a category X has a structural action on itself which is, furthermore, strong with respect to itself. Such categories are essentially the subject matter of this section. To be reasonable, the strength transformations must satisfy various coherence conditions. When these are written out they are very similar to the conditions governing a symmetric tensor product. There are, however, two major differences: first, the associativity map is not an isomorphism, and second, the unit (called an empty context) does not have an identity action on either side. (Note that in the case of bang actions these are not isomorphisms.) This, of course makes it necessary to write down explicitly many coherence diagrams which would otherwise be implied.

A category with a strong structural action on itself has a natural transformation:

θ _{⊘} : X ⊘ (Y ⊘ Z) ⟶ (X ⊘ Y) ⊘ (X ⊘ Z)

such that e = θ _{⊘} ; e ⊘ e and d; 1 ⊘ θ _{⊘} ; θ _{⊘} = θ _{⊘} ; d ⊘ d. Rather than dealing with the strength of θ _{⊘} we may work with the linear strengths in each argument:

a_{⊘} = θ _{⊘} ; 1 ⊘ e: X ⊘ (Y ⊘ Z) ⟶ (X ⊘ Y) ⊘ Z

to be thought of as an associativity map and

c_{⊘} = θ _{⊘} ; e ⊘ 1: X ⊘ (Y ⊘ Z) ⟶ Y ⊘ (X ⊘ Z)

to be thought of as a symmetry map. We note that θ _{⊘} can then be reconstituted as:

θ _{⊘} = d; 1 ⊘ a_{⊘}; c_{⊘} = d; 1 ⊘ c_{⊘}; a_{⊘}.

Thus, in axiomatizing such a setting we may organize the axioms around the linear strengths of associativity and symmetry. Our first major test of the axiomatization will be to recover the strength of θ _{⊘} from its linear strengths (see Proposition 2.9).

In the following the reader should have in mind standard simple actions and bang actions: both are examples of context categories.

2.1 The definition A context category is a category equipped with a structural action

⊘ : X × X ⟶ X

and an empty context ⊤ and natural transformations:

a_{⊘}: X ⊘ (Y ⊘ Z) ⟶ (X ⊘ Y) ⊘ Z
c_{⊘}: X ⊘ (Y ⊘ Z) ⟶ Y ⊘ (X ⊘ Z)
lift: X ⟶ ⊤ ⊘ X
read: X ⊘ ⊤ ⟶ X

satisfying a number of coherence diagrams, as given below.

Empty context:

[figure: ⊤ ⊘ ⊤; X ⊘ (⊤ ⊘ Y); a_{⊘}; (X ⊘ ⊤) ⊘ Y; lift; read; 1 ⊘ lift; read ⊘1; ⊤; ⊤; X ⊘ Y; X ⊘ Y]

lift; read = 1  (4)
1 ⊘ lift; a_{⊘}; read ⊘1 = 1  (5)

Symmetry: [figure: X ⊘ (Y ⊘ Z); X ⊘ (Y ⊘ Z); X ⊘ Z; c_{⊘}; c_{⊘}; d; d; Y ⊘ (X ⊘ Z); X ⊘ (X ⊘ Z); c_{⊘}; X ⊘ (X ⊘ Z)]

c_{⊘}; c_{⊘} = 1  (6)
d; c_{⊘} = d  (7)

Elimination, duplication and lifting:

[figure: X; lift; ⊤ ⊘ X; X; lift; ⊤ ⊘ X; lift; lift; e; ⊤ ⊘ X; d; ⊤ ⊘ (⊤ ⊘ X); X]

lift; d = lift; lift  (8)
1 = lift; e  (9)

Transpositions:

[figure: X ⊘ (Y ⊘ Z); 1 ⊘ d; d; X ⊘ (X ⊘ (Y ⊘ (Y ⊘ Z))); 1 ⊘ c_{⊘}; X ⊘ (Y ⊘ (X ⊘ (Y ⊘ Z))); a_{⊘}; a_{⊘}; 1 ⊘ a_{⊘}; (X ⊘ Y) ⊘ Z; d; (X ⊘ Y) ⊘ ((X ⊘ Y) ⊘ Z); A ⊘ (B ⊘ Z); 1 ⊘ d; d; A ⊘ (A ⊘ (B ⊘ (B ⊘ Z))); 1 ⊘ c_{⊘}; A ⊘ (B ⊘ (A ⊘ (B ⊘ Z))); c_{⊘}; c_{⊘}; 1 ⊘ (1 ⊘ c_{⊘}); B ⊘ (A ⊘ Z); 1 ⊘ d; d; B ⊘ (B ⊘ (A ⊘ (A ⊘ Z))); 1 ⊘ c_{⊘}; B ⊘ (A ⊘ (B ⊘ (A ⊘ Z)))]

a_{⊘}; d = 1 ⊘ d; d; 1 ⊘ c_{⊘}; a_{⊘}; 1 ⊘ a_{⊘}  (10)
c_{⊘}; 1 ⊘ d; d; 1 ⊘ c_{⊘} = 1 ⊘ d; d; 1 ⊘ c_{⊘}; c_{⊘}; 1 ⊘ (1 ⊘ c_{⊘})  (11)

Bistrengths of the action:

[figure: X ⊘ (Y ⊘ (A ⊘ B)); 1 ⊘ c_{⊘}; X ⊘ (A ⊘ (Y ⊘ B)); c_{⊘}; a_{⊘}; Y ⊘ (X ⊘ (A ⊘ B)); 1 ⊘ a_{⊘}; Y ⊘ ((X ⊘ A) ⊘ B); c_{⊘}; (X ⊘ A) ⊘ (Y ⊘ B)]

This ensures that θ _{⊘} is a contextual strength (see 2.9).

c_{⊘}; 1 ⊘ a_{⊘}; c_{⊘} = 1 ⊘ c_{⊘}; a_{⊘}  (12)

Strong transformations:

[figure: X ⊘ Y; 1⊘lift; X ⊘ (⊤ ⊘ Y); X ⊘ (Y ⊘ ⊤); 1⊘read; X ⊘ Y; lift; c_{⊘}; a_{⊘}; read; ⊤ ⊘ (X ⊘ Y); (X ⊘ Y) ⊘ ⊤]

1 ⊘ lift; c_{⊘} = lift  (13)
a_{⊘}; read = 1 ⊘ read  (14)

Elimination of strengths:

[figure: X ⊘ (Y ⊘ Z); a_{⊘}; (X ⊘ Y) ⊘ Z; X ⊘ (Y ⊘ Z); c_{⊘}; Y ⊘ (X ⊘ Z); e; e ⊘ 1; e; 1 ⊘ e; Y ⊘ Z; Y ⊘ Z]

a_{⊘}; e ⊘ 1 = e  (15)
c_{⊘}; 1 ⊘ e = e  (16)

Duplication of strengths:

[figure: X ⊘ (Y ⊘ Z); d; X ⊘ (X ⊘ (Y ⊘ Z)); X ⊘ (Y ⊘ Z); d; X ⊘ (X ⊘ (Y ⊘ Z)); a_{⊘}; 1 ⊘ a_{⊘}; a_{⊘}; c_{⊘}; 1 ⊘ c_{⊘}; c_{⊘}; (X ⊘ Y) ⊘ Z; d⊘1; (X ⊘ (X ⊘ Y)) ⊘ Z; Y ⊘ (X ⊘ Z); 1⊘d; Y ⊘ (X ⊘ (X ⊘ Z))]

d; 1 ⊘ a_{⊘}; a_{⊘} = a_{⊘}; d ⊘ 1  (17)
d; 1 ⊘ c_{⊘}; c_{⊘} = c_{⊘}; 1 ⊘ d  (18)

Associativity of strengths:

[figure: X ⊘ (Y ⊘ (Z ⊘ W)); a_{⊘}; (X ⊘ Y) ⊘ (Z ⊘ W); 1 ⊘ a_{⊘}; a_{⊘}; X ⊘ ((Y ⊘ Z) ⊘ W); a_{⊘}; (X ⊘ (Y ⊘ Z)) ⊘ W; a_{⊘}⊘1; ((X ⊘ Y) ⊘ Z) ⊘ W; X ⊘ (Y ⊘ (Z ⊘ W)); c_{⊘}; Y ⊘ (X ⊘ (Z ⊘ W); 1⊘a_{⊘}; Y ⊘ ((X ⊘ Z) ⊘ W)); 1 ⊘ a_{⊘}; a_{⊘}; X ⊘ ((Y ⊘ Z) ⊘ W); a_{⊘}; (X ⊘ (Y ⊘ Z)) ⊘ W; c_{⊘}⊘1; (Y ⊘ (X ⊘ Z)) ⊘ W]

1 ⊘ a_{⊘}; a_{⊘}; a_{⊘} ⊘ 1 = a_{⊘}; a_{⊘}  (19)
1 ⊘ a_{⊘}; a_{⊘}; c_{⊘} ⊘ 1 = c_{⊘}; 1 ⊘ a_{⊘}; a_{⊘}  (20)

Symmetry of strengths:

[figure: X ⊘ (Y ⊘ (Z ⊘ W)); c_{⊘}; Y ⊘ (X ⊘ (Z ⊘ W)); 1⊘c_{⊘}; Y ⊘ (Z ⊘ (X ⊘ W)); 1 ⊘ a_{⊘}; a_{⊘}; X ⊘ ((Y ⊘ Z) ⊘ W); c_{⊘}; (Y ⊘ Z) ⊘ (X ⊘ W); X ⊘ (Y ⊘ (V ⊘ Z)); 1⊘c_{⊘}; X ⊘ (V ⊘ (Y ⊘ Z)); c_{⊘}; V ⊘ (X ⊘ (Y ⊘ Z)); c_{⊘}; 1 ⊘ c_{⊘}; Y ⊘ (X ⊘ (V ⊘ Z)); 1⊘c_{⊘}; Y ⊘ (V ⊘ (X ⊘ Z)); c_{⊘}; V ⊘ (Y ⊘ (X ⊘ Z))]

1 ⊘ a_{⊘}; c_{⊘} = c_{⊘}; 1 ⊘ c_{⊘}; a_{⊘}  (21)
1 ⊘ c_{⊘}; c_{⊘}; 1 ⊘ c_{⊘} = c_{⊘}; 1 ⊘ c_{⊘}; c_{⊘}  (22)

Lifting of strengths:

[figure: X ⊘ Y; lift; ⊤ ⊘ (X ⊘ Y); X ⊘ Y; lift; ⊤ ⊘ (X ⊘ Y); lift ⊘1; a_{⊘}; 1 ⊘ lift; c_{⊘}; (⊤ ⊘ X) ⊘ Y; X ⊘ (⊤ ⊘ Y)]

Note that the second of these diagrams has already occurred to ensure the strong naturality for lift.

lift; a_{⊘} = lift ⊘1  (23)

Remark 2.1 (Unitless context categories)

If we drop all references to the empty context ⊤ above, we arrive at the notion of a “unitless context category”, or a “context category without empty context”. For the most part we shall not consider such context categories, but we shall see some unitless examples later. □

First it is obvious how to interpret a cartesian category with its standard simple action as a context category. We shall refer to these examples as simple context categories. They are equivalently specified by the additional requirement that the strength transformations a_{⊘}, read, and lift are isomorphisms. This latter is the interpretation of the word “simple” that we have in mind in the discussion of context. Lemma 2.2 In a simple context category, X ⊘ Y is a cartesian product. Proof. The fact that a_{⊘}, read, and lift are isomorphisms immediately means that X ⊘ Y is a symmetric tensor. Duplication and elimination turns each object into a natural commutative comonoid. However, a symmetric tensor with a natural commutative comonoid structure is a product. □

With a view to understanding how a bang action gives a context category, we note that there are many examples of unitless context categories.

Suppose Y is a symmetric monoidal category and F: Y ⟶ Y gives a commutative monoidal structural action. Clearly, the role of c_{⊘} can be filled using the symmetric map of the tensor; note (6), (7), (11), (16), (18), and (22) will then automatically be satisfied. If the functor F has a tensorial strength then there is an obvious candidate for the associativity:

(a_{⊗})^{−1}; θ^{F} ⊗ 1: F (X) ⊗ (F (Y) ⊗ Z) ⟶ F (F (X) ⊗ Y) ⊗ Z.

With this definition (12), (15), (17), (19), (20), and (21) are easy consequences. This leaves (4), (8), (9), (10), (13), (14), and (23) to be satisfied. All these except (10) involve the empty context.

(10) is satisfied if the following diagram commutes:

[figure: F (X) ⊗ F (Y); Δ⊗Δ; ς; (F (X) ⊗ F (Y)) ⊗ (F (X) ⊗ F (Y)); θ^{F}; θ^{F} ⊗ θ^{F}; F (F (X) ⊗ Y); Δ; F (F (X) ⊗ Y) ⊗ F (F (X) ⊗ Y)]

where ς is the obvious exchange map. Proposition 2.3 If Y is a symmetric monoidal category and F: Y ⟶ Y is a commutative monoidal structural action which has a symmetric monoidal strength relative to F such that

Δ ⊗ Δ; ς; θ^{F} ⊗ θ^{F} = θ^{F}; Δ

then Y is a unitless context category with X ⊘ Y = F (X) ⊗ Y.

In a cartesian tensor category (that is a tensor category with ⊗ = ×) this extra condition is always satisfied as in this setting Δ ⊗ Δ; ς = Δ and naturality of Δ gives the desired square. Thus, we have: Corollary 2.4 If Y is a cartesian category and F: Y ⟶ Y has a cartesian strength then Y is a unitless context category with X ⊘ Y = F (X) × Y.

The categorical interpretation of the bang functor in MELL categories [B95] requires that it be a monoidal cotriple whose (free) coalgebras are naturally commutative comonoids. This means the functor gives a symmetric monoidal structural action and a strength relative to itself. For example, the map a_{⊘} is the canonical map ! X ⊗ ( ! Y ⊗ Z) ⟶ ( ! X ⊗ ! Y) ⊗ Z ⟶ ( !! X ⊗ ! Y) ⊗ Z ⟶ ! ( ! X ⊗ Y) ⊗ Z. (Note that this is not an isomorphism.) Further, the extra condition of the proposition is an easy consequence of the coherence requirement that d ⊗ d; ς; m_{⊗} ⊗ m_{⊗} = m_{⊗}; d. Thus, the bang action already gives a unitless context category.

To obtain an interpretation of the empty context we need to describe the read and lift maps:

lift = (uL_{⊗})^{−1}; m_{⊤} ⊗ 1: X ⟶ ! ⊤ ⊗ X

read = uR_{⊗}; ϵ: ! X ⊗ ⊤ ⟶ X.

(Again, note these are not isomorphisms.)

Finally we must check (4), (8), (9), (13), (14), and (23) for this definition of the maps. This is an easy exercise which we leave to the reader (see [B95], [Be94], or [BCS92] for the relevant coherence conditions). Proposition 2.5 Any MELL category is a context category with respect to the bang action.

2.2 Contextual modules It is reasonable to ask what a contextual action of a context category X must look like. We shall call contextual actions contextual modules or simply X–modules when X is understood to be a context category. A module is an action, as before, but is equipped not only with elimination and duplication but also a lifting, associativity, and symmetry map. Note that the read map cannot be assumed as part of the structure of a contextual module, as the typing of its domain and codomain would make no sense if X were not acting on itself. The diagrams which must be satisfied are all the diagrams above less (4) and (14) (which would demand that ⊤ is in the module).

A simple contextual module is an X–module Y in which X is a simple context category and such that the strength transformations a_{⊘} and lift are isomorphisms. In particular this means that ⊤ ⊘ Y is naturally isomorphic to Y, for any Y ∈ Y.

The strong functors between modules must now preserve the additional structure we have introduced. This gives three further diagrams (that is including elimination and duplication strength) to be satisfied by the strength transformation of the functors:

Associative strength:

[figure: X ⊘ (Y ⊘ F (Z)); 1⊘θ_{F}; θ_{F}; F (X ⊘ (Y ⊘ Z)); a_{⊘}; F (a_{⊘}); (X ⊘ Y) ⊘ F (Z); θ_{F}; F ((X ⊘ Y) ⊘ Z)]

Symmetric strength:

[figure: X ⊘ (Y ⊘ F (Z)); 1⊘θ_{F}; θ_{F}; F (X ⊘ (Y ⊘ Z)); c_{⊘}; F (c_{⊘}); Y ⊘ (X ⊘ F (Z)); 1⊘θ_{F}; θ_{F}; F (Y ⊘ (X ⊘ Z))]

Lifting strength:

[figure: F (X); lift; ⊤ ⊘ F (X); F (lift); θ_{F}; F (⊤ ⊘ X)]

A functor (with strength) which satisfies the structural strength conditions together with the above will be called contextually strong.

It is clear that we may now form a 2–category of X–modules, contextually strong functors, and strong transformations: Proposition 2.6 X–modules, contextually strong functors, and strong transformations form a 2–category Context(X).

Again the only point that needs comment concerns the composition of contextually strong functors. Clearly we may define

(F, θ_{F}) ∘ (G, θ_{G}) = (F ∘ G, θ_{G}; G(θ_{F}))

and we leave it as an exercise for the reader to check that the five strength requirements are satisfied by the composite strength.

In order to explain what these requirements mean at the fibrational level we must make the action itself part of the fibrational information. The point is that a context category has a natural structural action on itself and so gives rise to a structural fibration. This structural fibration acts as a fibration on the fibration arising from the module. The desire to have the action represented at the level of the fibrations is, therefore, the motivation behind this notion of contextually strong. As we shall see, this pattern of “self-strengthening” will be repeated.

The property of being an X–module transfers both onto the Eilenberg-Moore category of strong cotriples and onto the Kleisli category of strong triples. Proposition 2.7 Context(X) has

(i) the Eilenberg-Moore construction for cotriples, (ii) the Kleisli construction for triples.

Proof. (i) Suppose (S, ϵ, δ) is a contextually strong cotriple on an X–module Y. Then an arbitrary object of the Eilenberg–Moore category is ν: Y ⟶ S(Y) satisfying the usual diagrams. However, this gives

X ⊘ Y ⟶^{ν} S(X ⊘ Y) = X ⊘ Y ⟶^{1 ⊘ ν} X ⊘ S(Y) ⟶^{θ_{S}} S(X ⊘ Y)

which is also a coalgebra, since the following commute:

[figure: X ⊘ Y; X ⊘ Y; 1⊘ν; X ⊘ S(Y); θ_{S}; S(X ⊘ Y); 1 ⊘ ν; 1 ⊘ ν; 1 ⊘ S(ν); S(1 ⊘ ν); X ⊘ S(Y); 1⊘ϵ; X ⊘ Y; X ⊘ S(Y); 1⊘δ; X ⊘ S(S(Y)); θ_{S}; S(X ⊘ S(Y)); θ_{S}; ϵ; θ_{S}; S(θ_{S}); S(X ⊘ Y); S(X ⊘ Y); δ; S(S(X ⊘ Y))]

In each case, the bottom diagrams commute by the strength of ϵ, δ, and the top diagrams commute because ν is a coalgebra (and θ is natural, in the case of the right-hand diagram).

Furthermore this is a contextual action as it is given by the action of X on itself.

(ii) In a similar manner the Kleisli category may be turned into an X–module. The objects of the Kleisli category are just the objects of the original module, thus there is a natural candidate for ingredients of a contextual action, which is the underlying action on objects, and post-composing with θ gives the action on algebra morphisms. We must verify that all the context category structure lifts naturally to the Kleisli category.

The main point is this: strength θ_{T}: X ⊘ T (Y) ⟶ T (X ⊘ Y) is (exactly) a distribution for the functor X ⊘ and this ensures the action lifts to the Kleisli category. Furthermore the fact that the contextual structural transformations are strong means that they “commute” with this distribution, which ensures that they all lift to natural transformations in the Kleisli category, by the standard Kleisli comparison functor. Thus, each structure map becomes the underlying map post-composed with η, the unit of the triple, e.g. e in the Kleisli category is e; η, the image of e under the Kleisli comparison functor. Finally the necessary coherence diagrams are induced by their counterparts in the underlying category. This shows that the Kleisli category is a contextual module. □

An example of this is given by the Kleisli construction for a (product) strong triple. A strong triple in this sense is just a contextual triple for the standard simple action of a cartesian category on itself. The proposition tells us that the Kleisli category is a contextual module.

Before leaving this example it is worth briefly mentioning an interesting aspect which is a consequence of this observation. As the Kleisli category has the same objects as X, this means at the level of objects we have an operation given by the action. Further, this operation is functorial in the second argument for each fixed entry in the first argument (as it is the action) and the symmetry of the product allows one to conclude that it is also functorial in the first argument for each fixed entry in the second argument. However, it is not a functor of two arguments as the interchange law does not hold. This “shuffle” tensor structure was used by Power and Robinson [PR96] to characterize Moggi’s computational monads [M89]. They argued that the notion of a “shuffle” tensor (they used the terms “binoidal” and “premonoidal”) was usefully more general as it captured (among other things) elementary control structures.

A contextual line is a contextual module generated by a single object. For any simple contextual module Y we may obtain a contextual line by considering the least full submodule containing Y. This we call the contextual line generated by Y. Observe that we obtain essentially the same basic structure as observed by Power and Robinson: their cartesian based structures—which include elementary control structures—are simple contextual lines.

Notice, however, that our approach has an orientation complementary to that of Power and Robinson, and indeed to most of the work on action calculi. Rather than build up the structure from an action, as suggested here, they take the total structure and, essentially, extract the action. Thus, the center of a premonoidal category always has a tensor action on the whole category, and elementary control structures have a cartesian category at their center. With a cartesian center, since all objects can be generated from ones of the form X ⊗ ⊤, this action provides a (simple) contextual line.

2.3 Contextual strength for functors of two arguments The requirements (15)–(23) can retrospectively now be seen as arising out of the demand that a_{⊘} and c_{⊘} be the linear contextual strengths for the functor ⊘ . Certainly, we have: Lemma 2.8 In a context category X for all objects Y and Z the following functors with strengths are contextually strong: ( ⊘ Z, a_{⊘}) and (Y ⊘ , c_{⊘}).

We now wish to establish that ⊘ as a functor of two arguments has a contextual strength. We shall accomplish this by proving the following important proposition which shows how the linear strengths for the single arguments of a two argument functor can be combined into a strength for the functor: Proposition 2.9 A functor F: Y_{1} × Y_{2} ⟶ Y between X–modules has a contextual strength θ_{F} if and only if

• F has linear contextual strengths fst: X ⊘ F (Y_{1}, Y_{2}) ⟶ F (X ⊘ Y_{1}, Y_{2}) and snd: X ⊘ F (Y_{1}, Y_{2}) ⟶ F (Y_{1}, X ⊘ Y_{2}),

• The linear strengths commute:

[figure: X ⊘ (Y ⊘ F (A, B)); 1 ⊘ snd; X ⊘ F (A, Y ⊘ B); c_{⊘}; fst; Y ⊘ (X ⊘ F (A, B)); 1⊘ fst; Y ⊘ F (X ⊘ A, B); snd; F (X ⊘ A, Y ⊘ B)]

This correspondence is a bijection. Furthermore a natural transformation between functors α: F (X, Y) ⟶ G(X, Y) is strong if and only if it is strong with respect to the (single argument) linear strengths.

This immediately explains the requirement (12) as this gives Corollary 2.10 In a context category, θ _{⊘} = d; 1⊘c_{⊘}; a_{⊘} is a contextual strength for the structural action. Proof (of 2.9). We start by assuming that θ is a contextual strength for F: our task is to show that

X ⊘ F (A, B) ⟶^{fst} F (X ⊘ A, B) = X ⊘ F (A, B) ⟶^{θ_{F}} F (X ⊘ A, X ⊘ B) ⟶^{F (1, e)} F (X ⊘ A, B)

will be a contextual strength. By symmetry this will allow us to conclude that snd: X ⊘ F (A, B) ⟶ F (A, X ⊘ B) will be a contextual strength. To establish the first direction of the equivalence it will then only remain to show that these linear strengths commute.

We need to check the five conditions for strength; we illustrate two cases:

Elimination strength:

fst; F (e, 1) = θ_{F}; F (1, e); F (e, 1) = θ_{F}; F (e, e) = e.

Associative strength:

1 ⊘ fst; fst; F (a_{⊘}, 1) = 1 ⊘ (θ_{F}; F (1, e)); θ_{F}; F (1, e); F (a_{⊘}, 1)
= 1 ⊘ θ_{F}; θ_{F}; F (1, 1 ⊘ e); F (1, e); F (a_{⊘}, 1)
= 1 ⊘ θ_{F}; θ_{F}; F (a_{⊘}, 1 ⊘ e; e)
= 1 ⊘ θ_{F}; θ_{F}; F (a_{⊘}, e; e)
= 1 ⊘ θ_{F}; θ_{F}; F (a_{⊘}, a_{⊘}; e ⊘ 1; e)
= 1 ⊘ θ_{F}; θ_{F}; F (a_{⊘}, a_{⊘}); F (1, e ⊘ 1; e)
= a_{⊘}; θ_{F}; F (1, e)
= a_{⊘}; fst

It is easy to verify that the linear strengths so defined commute.

For the converse we now assume that we have the linear strengths which commute and will establish that

X ⊘ F (A, B) ⟶^{θ_{F}} F (X ⊘ A, X ⊘ B)

= X ⊘ F (A, B) ⟶^{d} X ⊘ (X ⊘ F (A, B)) ⟶^{1 ⊘ snd} X ⊘ F (A, X ⊘ B) ⟶^{fst} F (X ⊘ A, X ⊘ B)

is a contextual strength. Again we must check the five conditions governing strength. We shall illustrate with three cases. One equation used frequently in the proof is the following:

1 ⊘ θ_{F}; θ_{F} = 1 ⊘ d; d; 1 ⊘ c_{⊘}; 1 ⊘ (1 ⊘ (1 ⊘ snd; snd)); 1 ⊘ fst; fst

which uses the fact that the linear strengths commute to re-express the process of moving contexts inside.

Duplication strength:

d; 1 ⊘ θ_{F}; θ_{F} = d; 1 ⊘ d; d; 1 ⊘ c_{⊘}; 1 ⊘ (1 ⊘ (1 ⊘ snd; snd)); 1 ⊘ fst; fst
= d; d; 1 ⊘ d; 1 ⊘ c_{⊘}; 1 ⊘ (1 ⊘ (1 ⊘ snd; snd)); 1 ⊘ fst; fst
= d; d; 1 ⊘ d; 1 ⊘ (1 ⊘ (1 ⊘ snd; snd)); 1 ⊘ fst; fst
= d; d; 1 ⊘ (1 ⊘ d); 1 ⊘ (1 ⊘ (1 ⊘ snd; snd)); 1 ⊘ fst; fst
= d; d; 1 ⊘ (1 ⊘ snd); 1 ⊘ (1 ⊘ F (1, d)); 1 ⊘ fst; fst
= d; 1 ⊘ snd; 1 ⊘ F (1, d); d; 1 ⊘ fst; fst
= d; 1 ⊘ snd; 1 ⊘ F (1, d); fst; F (d, 1)
= d; 1 ⊘ snd; fst; F (d, d)

Commutative strength:

1 ⊘ θ_{F}; θ_{F}; F (c_{⊘}, c_{⊘}) = 1 ⊘ d; d; 1 ⊘ c_{⊘}; 1 ⊘ (1 ⊘ (1 ⊘ snd; snd)); 1 ⊘ fst; fst; F (c_{⊘}, c_{⊘})
= 1 ⊘ d; d; 1 ⊘ c_{⊘}; 1 ⊘ (1 ⊘ (1 ⊘ snd; snd)); c_{⊘}; 1 ⊘ (1 ⊘ F (1, c_{⊘}));
1 ⊘ fst; fst
= 1 ⊘ d; d; 1 ⊘ c_{⊘}; c_{⊘}; 1 ⊘ (1 ⊘ c_{⊘}); 1 ⊘ (1 ⊘ (1 ⊘ snd; snd));
1 ⊘ fst; fst
= c_{⊘}; 1 ⊘ d; d; 1 ⊘ c_{⊘}; 1 ⊘ (1 ⊘ (1 ⊘ snd; snd)); 1 ⊘ fst; fst
= c_{⊘}; 1 ⊘ θ_{F}; θ_{F}

Notice the use of the transposition identity (11) to bring the symmetry map out in the penultimate step.

Lifting strength:

lift; θ_{F} = lift; d; 1 ⊘ snd; fst
= lift; lift; 1 ⊘ snd; fst
= lift; snd; lift; fst
= F (1, lift); F (lift, 1)
= F (lift, lift)

Note the use of (8) in the first step.

It would be strange indeed if the re-expression of a bistrength in terms of its linear strengths (and vice-versa) did not yield the bistrength itself. We now verify that these transitions are indeed inverses of each other. First we assume we are given the bistrength and reconstitute it from its components:

θ_{F} = d; 1 ⊘ snd; fst
= d; 1 ⊘ (θ_{F}; F (e, 1)); θ_{F}; F (1, e)
= d; 1 ⊘ θ_{F}; θ_{F}; F (1 ⊘ e, e)
= θ_{F}; F (d; 1 ⊘ e, d; e)
= θ_{F}

Next we assume we have the linear strengths and verify that extracting the linear strengths from the bistrength that we build does give back the original linear strengths:

fst = θ_{F}; F (1, e)
= d; 1 ⊘ fst; snd; F (1, e)
= d; 1 ⊘ fst; e
= d; e; fst
= fst

snd = θ_{F}; F (e, 1)
= d; 1 ⊘ snd; fst; F (e, 1)
= d; 1 ⊘ snd; e
= d; e; snd
= snd

The final statement of the proposition dealing with natural transformations is straightforward to verify. □

For example, in the 2–category Context(X) the trivial category 1 of one object and one map (the identity) with the trivial action is a final object. Functors from it pick out objects as usual and have strength

e: X ⊘ F (1) ⟶ F (X ⊘ 1) = F (1),

thus the above result is just the analogue of the classical result concerning bifunctors.

2.4 Storage in context categories Suggestively we shall adopt the convention, in any context category, of writing \overline{!} (X) = X ⊘ ⊤. Notice that we have:

\overline{!} (X) ⟶^{δ} \overline{!} ( \overline{!} (X)) = X ⊘ ⊤ ⟶^{1 ⊘ lift} X ⊘ (⊤ ⊘ ⊤) ⟶^{a_{⊘}} (X ⊘ ⊤) ⊘ ⊤

and

\overline{!} (X) ⟶^{ϵ} X = X ⊘ ⊤ ⟶^{read} X.

Lemma 2.11 In any context category ( \overline{!} ( ), ϵ, δ) is a cotriple. Proof. We must show that δ; \overline{!} (ϵ) = δ; ϵ = 1 and δ; δ = δ; \overline{!} (δ).

The first counit identity δ; \overline{!} (ϵ) = 1 is (when translated) (5) above.

For the second counit identity we have:

[figure: X ⊘ ⊤; 1 ⊘ lift; X ⊘ (⊤ ⊘ ⊤); a_{⊘}; (X ⊘ ⊤) ⊘ ⊤; 1 ⊘ read; read; X ⊘ ⊤]

where the left triangle is (4) and the right triangle commutes as read is strong – (14) above. Finally for the associativity of comultiplication we have:

[figure: X ⊘ ⊤; 1 ⊘ lift; X ⊘ \overline{!} (⊤); a_{⊘}; \overline{!} ( \overline{!} (X)); 1 ⊘ (1 ⊘ lift); (B); 1 ⊘ lift; 1 ⊘ lift; (A); X ⊘ (⊤ ⊘ \overline{!} (⊤)); a_{⊘}; \overline{!} (X) ⊘ \overline{!} (⊤); 1 ⊘ a_{⊘}; X ⊘ \overline{!} (⊤); 1⊘(lift ⊘1); X ⊘ \overline{!} ( \overline{!} (⊤)); (D); a_{⊘}; a_{⊘}; (C); a_{⊘} ⊘ 1; \overline{!} ( \overline{!} (X)); (1⊘ lift)⊘1; \overline{!} (X ⊘ \overline{!} (⊤)); a_{⊘} ⊘ 1; \overline{!} ( \overline{!} ( \overline{!} (X)))]

where the cell (A) commutes using the naturality of lift to obtain the equality:

lift; lift = lift; 1 ⊘ lift

and the fact that lift is strong (13) which says lift; a_{⊘} = lift ⊘1; these allow

lift; 1 ⊘ lift; a_{⊘} = lift; lift; a_{⊘}
= lift; lift ⊘1

Squares (B) and (C) commute by naturality, (D) uses the associativity pentagon (19). □

We note that the storage cotriple gives rise to a module for the Eilenberg-Moore coalgebras. In a strong sense the empty context is a vestige of a missing tensor structure. We now consider

how such structure may be added. We shall identify the tensor unit and the empty context. Clearly this and the tensor product ⊗ must be contextually strong as functors. This means we must have the following strength maps:

θ_{⊤}: X ⊘ ⊤ ⟶ ⊤
θ _{⊗} : X ⊘ (Y ⊗ Z) ⟶ (X ⊘ Y) ⊗ (X ⊘ Z)

The first map has to coincide with the elimination map e_{X,⊤} (in order to satisfy the “elimination strength” diagram). We may break the second map into two components:

fst_{⊗} = θ _{⊗Z}: X ⊘ (Y ⊗ Z) ⟶ (X ⊘ Y) ⊗ Z
snd_{⊗} = θ_{Y ⊗} : X ⊘ (Y ⊗ Z) ⟶ Y ⊗ (X ⊘ Z)

We require that the tensor unit isomorphisms and the tensor associativity isomorphism a_{⊗} be strong. So, the following diagrams must commute.

[figure: X ⊘ Y; 1 ⊘ u_{⊗}^{R}; X ⊘ (Y ⊗ ⊤); X ⊘ Y; 1 ⊘ u_{⊗}^{L}; X ⊘ (⊤ ⊗ Y); u_{⊗}^{R}; fst_{⊗}; u_{⊗}^{L}; snd_{⊗}; (X ⊘ Y) ⊗ ⊤; ⊤ ⊗ (X ⊘ Y)]

[figure: A ⊘ (X ⊗ (B ⊗ Y)); 1 ⊘ a_{⊗}; A ⊘ ((X ⊗ B) ⊗ Y); snd_{⊗}; fst_{⊗}; X ⊗ (A ⊘ (B ⊗ Y)); (A ⊘ (X ⊗ B)) ⊗ Y; 1 ⊗ fst_{⊗}; snd_{⊗} ⊗ 1; X ⊗ ((A ⊘ B) ⊗ Y); a_{⊗}; (X ⊗ (A ⊘ B)) ⊗ Y]

uR_{⊗} = 1 ⊘ uR_{⊗}; fst_{⊗}  (24)
uL_{⊗} = 1 ⊘ uL_{⊗}; snd_{⊗}  (25)
1 ⊘ a_{⊗}; fst_{⊗}; snd_{⊗} ⊗1 = snd_{⊗}; 1 ⊗ fst_{⊗}; a_{⊗}  (26)

With this equipment we arrive at a contextual monoidal category. It is worth noting that if we make the single argument (linear) components of the strength of the tensor (that is, fst and snd) isomorphisms, then we will turn the structural action into a monoidal structural action, for then

X ⊘ Y ⟶^{1⊘(u_{⊗}^{L})^{−1}} X ⊘ (⊤ ⊗ Y) ⟶^{fst_{⊗}} \overline{!} X ⊗ Y

is a natural isomorphism. The next result shows \overline{!} is always a commutative comonoid. Recall from the discussion preceding Lemma 1.3 the notion of a functor being a comonoid. Proposition 2.12 In any contextual monoidal category X, if (Y, Δ, ι) is a commutative comonoid (where Y is an object), then

( ⊘ Y: X ⟶ X, 1 ⊘ Δ; θ_{⊗}, e; ι)

is a commutative comonoid.

In other words the category of (commutative) comonoids of a contextual monoidal category is a module: picking a particular comonoid allows one to obtain a line of comonoids. Proof. Define the comultiplication by

X ⊘ Y \underrightarrow{Δ′} (X ⊘ Y) ⊗ (X ⊘ Y) = X ⊘ Y \underrightarrow{1 ⊘ Δ} X ⊘ (Y ⊗ Y) \underrightarrow{θ _{⊗}} (X ⊘ Y) ⊗ (X ⊘ Y)

and the counit by

X ⊘ Y \underrightarrow{e′} ⊤ = X ⊘ Y \underrightarrow{e} Y \underrightarrow{ι} ⊤.

That Δ′; 1 ⊗ e′ = (uR_{⊗})^{−1} and Δ; e′ ⊗ 1 = (uL_{⊗})^{−1} follows directly from the strength of uR_{⊗} and uL_{⊗}. It remains to check the coassociativity but this is a direct consequence of the strength of a_{⊗}.

Finally, the preservation of commutativity is given by the fact that context duplication is “commutative”, using the single argument (linear) strengths of the symmetry map for the tensor.

□

Clearly (u_{⊗})^{−1}: ⊤ ⟶ ⊤⊗⊤ is always a (commutative) comonoid, thus \overline{!} X = X ⊘⊤ is naturally a comonoid. It is interesting to note even when the monoidal category is not symmetric, there will be a sense in which \overline{!} X is a commutative comonoid. Corollary 2.13 In any contextual symmetric monoidal category, \overline{!} X is a commutative comonoid.

This observation is of some interest as it explains why bang functors should be expected to have a comonoid structure. Further given these observations it is reasonable to conjecture that a MELL category is, up to equivalence, the special case of a contextual symmetric monoidal category in which the structural action is made monoidal by demanding fst and snd be isomorphisms. We can see no obvious obstacle to verifying this, apart from the number of diagrams that must be checked. We leave this as a conjecture for the moment, delaying the proof to the sequel where proof circuits will make such proofs more transparent.

3 Structural bimodules and cocontext

The structure so far is the basis for our proposal to rest such notions as “computation in context” and “resource management” upon the fundamental notion of a strong action of a category upon itself. However, so far we have only enough structure to handle context in the hypothesis of a computation, or to handle “classical resource management” in the hypothesis. To achieve the symmetrical situation one might expect (say, upon viewing Girard’s unified logic), we must dualize our structure, so introducing the notion of cocontext. For the most part, this is straightforward, and we will content ourselves with a quicker summary than was done for context, leaving the emphasis for those places where the unexpected may occur. In the following section, whenever we refer to “the evident diagrams”, the reader ought to look for the corresponding diagrams above and dualize them.

3.1 Cocontext Suppose we have a category X acting on categories Y, Y′ via functors

⦸: Y × X ⟶ Y ⦸: Y′ × X ⟶ Y′

(we shall not distinguish between the actions, since it is generally obvious which action is relevant in any situation). Then a functor F: Y ⟶ Y′ is costrong if there is a natural transformation

θ: F (Y ⦸ X) ⟶ F (Y) ⦸ X

called a costrength. A costrong natural transformation between costrong functors is an ordinary natural transformation satisfying the evident diagram.

An action ⦸ is costructural if the functor ⦸ X is a triple for each X; this will induce these natural transformations (“contraction” and “introduction”):

b: (Y ⦸ Z) ⦸ Z ⟶ Y ⦸ Z
i: Y ⟶ Y ⦸ Z

satisfying the evident diagrams. In the obvious manner we extend the notion of a costrong functor to a costructural functor by adding the evident commutativity requirements.

Again, the situation where a category has a costrong costructural action on itself is of particular importance. We shall say a cocontext category is a category X equipped with costructural action

⦸: X × X ⟶ X

and an empty cocontext ⊥ and natural transformations

a_{⦸}: X ⦸ (Y ⦸ Z) ⟶ (X ⦸ Y) ⦸ Z
c_{⦸}: (X ⦸ Y) ⦸ Z ⟶ (X ⦸ Z) ⦸ Y
colift: X ⦸ ⊥ ⟶ X
coread: X ⟶ ⊥ ⦸ X

satisfying the evident commutativity diagrams. We can generalize this to the notion of an Xcomodule, which is an action equipped with contraction, introduction, associativity, symmetry, and colift, but not coread.

3.2 Bimodules A structural (X, Z)–bimodule, Y, is given by a structural action of X on Y (written X ⊘ Y) and a costructural action Z on Y (written Y ⦸ Z) such that in the Y coordinate each action is, respectively, costructurally costrong and structurally strong with respect to the other through the same natural transformation:

δ_{L}^{L}: X ⊘ (Y ⦸ Z) ⟶ (X ⊘ Y) ⦸ Z

which we shall call a cut distribution.

Notice that this strength/costrength requirement only makes sense on the bimodule coordinate as only on that coordinate are both actions defined. Later we consider the situation where the actions are defined on both arguments and this will lead to further strength/costrength cut distributions.

The natural transformations of the action must be strong or costrong as appropriate on their Y arguments. An example of a coherence diagram implied by the requirement that transformations be (co)structurally (co)strong is the following for contraction:

[figure: X ⊘ ((Y ⦸ Z) ⦸ Z); 1 ⊘ b; X ⊘ (Y ⦸ Z); δ_{L}^{L}; (X ⊘ (Y ⦸ Z)) ⦸ Z; δ_{L}^{L}; δ_{L}^{L} ⦸ 1; ((X ⊘ Y) ⦸ Z) ⦸ Z; b; (X ⊘ Y) ⦸ Z]

1 ⊘ b; δ_{L}^{L} = δ_{L}^{L}; δ_{L}^{L} ⦸ 1; b  (27)

Now if X is a context category and Z is a cocontext category we may strengthen the notion of a bimodule appropriately to mean a contextual action on the left and a cocontextual action on the right connected by a simultaneous contextual strength and cocontextual costrength transformation δ_{L}^{L}. This we will call a (X, Z)–contextual bimodule.

3.3 Fibrational forks and bimodules The main result of this section is that structural, and therefore contextual, bimodules give rise to fibrational forks. Note that as any contextual bimodule is a structural bimodule anything we establish for structural bimodules will be true for contextual bimodules.

We first define what will be the total category for this fibration.

Definition 3.1 Suppose Y is a structural (X, Z)–bimodule. StrBi(Y) is the category which is defined as follows:

Objects: These are triplets (X, Y, Z) of objects from X, Y, Z respectively, where X is referred to as the context, Z as the cocontext and Y as the active type.

Maps: Maps are triplets (f, α, g): (X, Y, Z) ⟶ (X′, Y′, Z′) such that f: X ⟶ X′ is a map of contexts, g: Z ⟶ Z′ is a map of cocontexts, and α: X ⊘ Y ⟶ Y′ ⦸ Z′ is a morphism of Y.

Identities: The identity maps are given by (1, e; i, 1): (X, Y, Z) ⟶ (X, Y, Z).

Composition: Composition is given as follows: (f, α, g); (f′, α′, g′) = (f; f′, β, g; g′) where β = d; (f ⊘ α); δ_{L}^{L}; (α′ ⦸ g′); b.

It is not obvious that this is a category: we must verify that the identity maps and composition behave in the correct manner. Proposition 3.2 StrBi(Y) as defined above is a category. Proof. For the identity laws we have (1, e; i, 1); (f, α, g) whose middle component is:

d; (1 ⊘ (e; i)); δ_{L}^{L}; (α ⦸ g); b = d; (1 ⊘ e); (1 ⊘ i); δ_{L}^{L}; (α ⦸ g); b
= (1 ⊘ i); δ_{L}^{L}; (α ⦸ g); b
= i; (α ⦸ g); b
= α; i; b
= α

and for the identity on the other side a dual argument. Note we have used the strength of the contraction transformation.

For the associativity of composition we consider

((f_{0}, α_{0}, g_{0}); (f_{1}, α_{1}, g_{1})); (f_{2}, α_{2}, g_{2}) = (f_{0}, α_{0}, g_{0}); ((f_{1}, α_{1}, g_{1}); (f_{2}, α_{2}, g_{2})).

The calculation for the middle map is as follows:

d; ((f_{0}; f_{1}) ⊘ (d; (f_{0} ⊘ α_{0}); δ_{L}^{L}; (α_{1} ⦸ g_{1}); b)); δ_{L}^{L}; (α_{2} ⦸ g_{2}); b
= d; (1 ⊘ d); ((f_{0}; f_{1}) ⊘ (f_{0} ⊘ α_{0})); (1 ⊘ δ_{L}^{L}); (1 ⊘ (α_{1} ⦸ g_{1})); (1 ⊘ b); δ_{L}^{L}; (α_{2} ⦸ g_{2}); b
= d; d; ((f_{0}; f_{1}) ⊘ (f_{0} ⊘ α_{0})); (1 ⊘ δ_{L}^{L}); (1 ⊘ (α_{1} ⦸ g_{1})); (1 ⊘ b); δ_{L}^{L}; (α_{2} ⦸ g_{2}); b
= d; (f_{0} ⊘ α_{0}); d; (f_{1} ⊘ δ_{L}^{L}); (1 ⊘ (α_{1} ⦸ g_{1})); (1 ⊘ b); δ_{L}^{L}; (α_{2} ⦸ g_{2}); b
= d; (f_{0} ⊘ α_{0}); d; (f_{1} ⊘ δ_{L}^{L}); (1 ⊘ (α_{1} ⦸ g_{1})); δ_{L}^{L}; (δ_{L}^{L} ⦸ 1); b; (α_{2} ⦸ g_{2}); b
= d; (f_{0} ⊘ α_{0}); d; (f_{1} ⊘ δ_{L}^{L}); δ_{L}^{L}; ((1 ⊘ α_{1}) ⦸ g_{1}); (δ_{L}^{L} ⦸ 1); b; (α_{2} ⦸ g_{2}); b
= d; (f_{0} ⊘ α_{0}); d; (f_{1} ⊘ δ_{L}^{L}); δ_{L}^{L}; ((1 ⊘ α_{1}) ⦸ g_{1}); (δ_{L}^{L} ⦸ 1); ((α_{2} ⦸ g_{2}) ⦸ g_{2}); b; b
= d; (f_{0} ⊘ α_{0}); d; (f_{1} ⊘ δ_{L}^{L}); δ_{L}^{L}; ((1 ⊘ α_{1}) ⦸ 1); (δ_{L}^{L} ⦸ 1); ((α_{2} ⦸ g_{2}) ⦸ (g_{1}; g_{2})); b ⦸ 1; b
= d; (f_{0} ⊘ α_{0}); d; (1 ⊘ δ_{L}^{L}); δ_{L}^{L}; ((f_{1} ⊘ α_{1}) ⦸ 1); (δ_{L}^{L} ⦸ 1); ((α_{2} ⦸ g_{2}) ⦸ 1); (b ⦸ (g_{1}; g_{2})); b
= d; (f_{0} ⊘ α_{0}); δ_{L}^{L}; (d ⦸ 1); ((f_{1} ⊘ α_{1}) ⦸ 1); (δ_{L}^{L} ⦸ 1); ((α_{2} ⦸ g_{2}) ⦸ 1); (b ⦸ (g_{1}; g_{2})); b
= d; (f_{0} ⊘ α_{0}); δ_{L}^{L}; ((d; (f_{1} ⊘ α_{1}); δ_{L}^{L}; (α_{2} ⦸ g_{2}); b) ⦸ (g_{1}; g_{2})); b

Note that the costrength of the duplication and the strength of the contraction transformation are fundamental to this proof as is the fact that δ_{L}^{L} provides both. □

There are two obvious functors

∂_{⊘}: StrBi(Y) ⟶ X; (f, α, g) ↦ f

and

∂_{⦸}: StrBi(Y) ⟶ Z; (f, α, g) ↦ g

Our main observation is that these functors form a fibrational fork^{3}. Definition 3.3 A fibrational fork is given by a fibration ∂: E ⟶ B together with a cofibration ∂′: E ⟶ B′ such that

• Each u: B ⟶ ∂(E) in B has a cartesian lifting which is ∂′-vertical. Each v: ∂′(E) ⟶ B′ in B′ has a cocartesian lifting which is ∂-vertical.

• In a commuting square in E,

[figure: X; f; Y; h; k; U; g; V]

where f,g are ∂′-vertical, h, k are ∂-vertical, if f,g are ∂-cartesian and k is ∂′-cocartesian then h is cocartesian.

The last bullet of the definition could have equivalently be expressed by requiring that for appropriately vertical arrows, the facts f is cartesian and h and k are cocartesian imply that g is cartesian. This says the cartesian substitution functors on the “cartesian fibres” are morphisms of the cofibration and conversely the cocartesian cosubstitution functors on the “cocartesian fibres” are morphisms of the fibration. A fibrational fork thus corresponds to a functor (in general a pseudo-functor) B^{op} × B′ ⟶ Cat.

We shall prove for StrBi(Y) that given any f: X ⟶ X′ and g: Z ⟶ Z′ and (X′, Y′, Z′) ∈ StrBi(Y), the following identity holds f^{∗}; g_{∗} = g_{∗}; f^{∗} (in general it suffices that there be a mediating isomorphism). This is sufficient to establish that we have a fibrational fork when the conditions of the first bullet hold, for the first bullet guarantees that considering fibres makes B^{op} × B′ ⟶ Cat (pseudo)functorial in each component, and the “interchange” identity f^{∗}; g_{∗} = g_{∗}; f^{∗} makes the map a (pseudo)functor of two variables. Proposition 3.4 ∂_{⊘}: StrBi(Y) ⟶ X, ∂_{⦸}: StrBi(Y) ⟶ Z is a fibrational fork. Proof.

(i) ∂_{⊘} is a fibration: The cartesian map over f: X ⟶ X′ is (f, e; i, 1): (X, Y, Z) ⟶ (X′, Y, Z). To establish this suppose (g; f, α, h): (X_{0}, Y_{0}, Z_{0}) ⟶ (X′, Y, Z); then

α = d; e; α; i; b
= d; (g ⊘ α); e; i; b
= d; (g ⊘ α); δ_{L}^{L}; (e ⦸ 1); i; b
= d; (g ⊘ α); δ_{L}^{L}; (e ⦸ 1); (i ⦸ 1); b
= d; (g ⊘ α); δ_{L}^{L}; ((e; i) ⦸ 1); b

3The definition of a fibrational fork is due to Benabou: we learnt of it through Bart Jacobs.

showing this map can be factorized and is uniquely determined by the factor.

Note also that it is a vertical map of ∂_{⦸}.

(ii) ∂_{⦸} is a cofibration: By a dual argument the cocartesian map over g: Z ⟶ Z′ is (1, e; i, g): (X, Y, Z) ⟶ (X, Y, Z′). This is always a vertical map for ∂_{⊘}.

(iii) These give a fibrational fork: we must show f^{∗}; g_{∗} = g_{∗}; f^{∗} for this we have:

d; (f ⊘ (e; i)); δ_{L}^{L}; ((e; i) ⦸ g); b = d; (1 ⊘ e); (f ⊘ i); δ_{L}^{L}; (e ⦸ g); (i ⦸ 1); b
= (f ⊘ i); δ_{L}^{L}; (e ⦸ g)
= (f ⊘ 1); (1 ⊘ i); δ_{L}^{L}; (e ⦸ 1); (1 ⦸ g)
= (f ⊘ 1); (1 ⊘ i); e; (1 ⦸ g)
= (f ⊘ 1); e; i; (1 ⦸ g)
= e; i
= d; (1 ⊘ (e; i)); δ_{L}^{L}; ((e; i) ⦸ 1); b

where the last step is obtained by reversing the steps above but substituting identities for f and g.

□

3.4 Morphisms of bimodules Given two (X, Z)–bimodules Y and Y′, we shall say a functor F: Y ⟶ Y′ is a morphism of bimodules in case F has a strength θ and costrength ϕ such that:

[figure: X ⊘ F (Y ⦸ Z); 1 ⊘ ϕ; X ⊘ (F (Y) ⦸ Z); δ_{L}^{L}; (X ⊘ F (Y)) ⦸ Z; θ; θ ⦸ 1; F (X ⊘ (Y ⦸ Z)); F (δ_{L}^{L}); F ((X ⊘ Y) ⦸ Z); ϕ; F (X ⊘ Y) ⦸ Z]

commutes. A natural transformation is a transformation of bimodule morphisms if it is strong and costrong in each variable. The reader may check that both structural and contextual bimodules, with morphisms of bimodules and transformations, form a 2–category. Notice that the appropriate notion of strength must be used in each case.

A morphism of (X, Z)–bimodules, F: Y ⟶ Y′, induces a morphism of the fibrational fork:

F̃: StrBi(Y) ⟶ StrBi(Y′); (f, α, g) ↦ (f, θ; F (α); ϕ, g).

A morphism of fibrational forks is a 1-cell in the 2–category of (product) cones over X and Z such that both the cartesian arrows and cocartesian arrows are preserved. Lemma 3.5 If F: Y ⟶ Y′ is a morphism of structural bimodules then F̃: StrBi(Y) ⟶ StrBi(Y′), as defined above is a morphism of fibrational forks. Proof. We must actually verify that F̃ is a functor: the fact that F̃ preserves identities can, in fact, be easily seen from the fact that it preserves cartesian and cocartesian arrows:

F̃(f, e; i, g) = (f, θ; F (e); F (i); ψ, g)
= (f, e; i, g).

Setting g to the identity shows cartesian arrows are preserved, setting f to the identity shows cocartesian arrows are preserved, and setting both to the identity shows identities are preserved.

It remains to show that composition is preserved:

F̃((f, α, g); (f′, α′, g′))
= F̃(f; f′, d; f ⊘ α; δ_{L}^{L}; α′ ⦸ g′; b, g; g′)
= (f; f′, θ; F (d; f ⊘ α; δ_{L}^{L}; α′ ⦸ g′; b); ϕ, g; g′)
= (f; f′, d; 1 ⊘ θ; θ; F (f ⊘ α; δ_{L}^{L}; α′ ⦸ g′); ϕ; ϕ ⦸ 1; b, g; g′)
= (f; f′, d; f ⊘ θ; θ; F (1 ⊘ α; δ_{L}^{L}; α′ ⦸ 1); ϕ; ϕ ⦸ g′; b, g; g′)
= (f; f′, d; f ⊘ θ; 1 ⊘ F (α); θ; F (δ_{L}^{L}); ϕ; F (α′) ⦸ 1; ϕ ⦸ g′; b, g; g′)
= (f; f′, d; f ⊘ (θ; F (α)); θ; F (δ_{L}^{L}); ϕ; (F (α′); ϕ) ⦸ g′; b, g; g′)
= (f; f′, d; f ⊘ (θ; F (α)); 1 ⊘ ϕ; δ_{L}^{L}; θ ⦸ 1; (F (α′); ϕ) ⦸ g′; b, g; g′)
= (f; f′, d; f ⊘ (θ; F (α); ϕ); δ_{L}^{L}; (θ; F (α′); ϕ) ⦸ g′; b, g; g′)
= F̃(f, α, g); F̃(f′, α′, g′)
□

To extract such an F from a morphism of fibrational forks requires that we use, as discussed for structural actions, the 2–category of fibrational forks with a morphism from a constant fibrational fork. This allows the reconstruction of the mere functor. To recover the strength and costrength, the structural and costructural fibrations must also be embedded constantly into the fibrational fork. A fibration over H: T ⟶ X can be lifted constantly in Z to a (X, Z)–fibrational fork by forming the product with Z, H × 1: T × Z ⟶ X × Z. These constantly lifted fibrations can be embedded into the fibrational fork by assuming that the appropriate side of the map in context and cocontext is trivial (using e and i).

The fact that it must be a morphism of bimodules (i.e. that it satisfies the above coherence diagram) can then be extracted from the preservation of the composition of (1, e, 1): (X, Y ⦸ Z, Z) ⟶ (X, Y, Z) with (1, i, 1): (X, Y, Z) ⟶ (X, X ⊘ Y, Z).

In a contextual bimodule, as for contextual modules, the action and the coaction themselves give rise to, respectively a fibred action and a cofibred coaction. This gives the contextual strength of the appropriate transformations but fails to secure the costrength at the bimodule argument. Thus, we strengthen the standard fibred action so that it acts constantly in each Z ∈ Z. The action then must give a morphism of fibrational forks:

⊘ : (StrAct(X) × Z) ×_{(X,Z)} StrBi(Y) ⟶ StrBi(Y)

where ×_{(X,Z)} is the product in the category of fibrational forks over (X, Z). This secures the bistrength of the bimodule argument for all the natural transformations.

This trick of strengthening and costrengthening the actions by ensuring that they are appropriately fibred will be applied again in the next section.

3.5 Bicontext categories We now understand contextual modules, cocontextual comodules and contextual bimodules. The final step is to introduce simultaneously contextual and cocontextual notions. An (X, Z)– bicontextual bimodule Y consists of a Z–cocontextual comodule X which is a (Z–costrong) context category with a (Z–costrong) contextual action on Y and a X–contextual module Z which is a (X–strong) cocontext category with a (X–strong) coaction on Y.

A bicontextual bimodule gives rise to a fibrational fork just as a bimodule does. However, what is new is that the context category X and the cocontext category Z are themselves (X, Z)-bimodules and generate fibrational forks. The action and coaction is then structure in the 2-category of fibrational forks. The fact that the actions are fibrational in this manner forces all the defining structure to be bistrong, that is, both contextually strong and cocontextually costrong with these strengths interacting appropriately.

All this is a bit of a mouthful and so we shall actually concentrate on the case when X = Z where the identification makes X a bicontext category, as explained below. We shall then refer to an (X, X)–bicontextual bimodule, where X is a bicontext category, as an X–bicontext bimodule.

Unwinding these ideas, a bicontext category is a category endowed with both context and cocontext structure. These structures must be linked with the following cut distributions, that is strength/costrength transformations:

δ_{L}^{L}: X ⊘ (Y ⦸ Z) ⟶ (X ⊘ Y) ⦸ Z
δ_{R}^{L}: X ⊘ (Y ⦸ Z) ⟶ Y ⦸ (X ⊘ Z)
δ_{L}^{R}: (X ⦸ Y) ⊘ Z ⟶ (X ⊘ Z) ⦸ Y

where δ_{L}^{L} (as already encountered) is the strength of the functor ⦸ Z, and simultaneously the costrength of the functor X ⊘ ; δ_{R}^{L} is the strength of the functor Y ⦸ ; and δ_{L}^{R} is the costrength of the functor ⊘ Z.

These must satisfy the coherence diagrams for bistrength (discussed below) in order to secure the fibrational enrichment. Remark 3.6 (Cut distributions) It is tempting to suppose that there should be another cut distribution δ_{R}^{R} : (X ⦸ Y) ⊘ Z ⟶ X ⦸(Y ⊘Z). However, it is immediately obvious that this makes no sense as a strength/costrength transformation. We will shortly see that the cut distributions, as their name suggests, correspond to cut rules in the sequent calculus we call the context calculus and which is the essence of Girard’s unified logic.

This suggests that there should be a corresponding “nonsense” cut rule missing from that system. This is indeed the case: to quote Girard [G93] “there is no possibility of defining a cut between two occurrences of A with a classical maintenance” in unified logic. □

To extract the coherence conditions of a bicontext category it is expedient to develop in parallel the notion of bistrength in bicontextual bimodules or, more specifically, in bicontext bimodules. Let X be a bicontext category, an X–bicontext bimodule is a category Z on which X has both an X–contextual action and an X–cocontextual coaction. This we call an X–biaction and must come equipped (as indeed must any bicontextual action–coaction pair) with the above cut distributions (notice that they are all correctly typed) which serve simultaneously as (contextual) strengths and (cocontextual) costrengths.

A morphism of (bicontext) bimodules F: Z ⟶ Z′ is a functor F equipped with a bistrength, that is a (contextual) strength θ and a (cocontextual) costrength ϕ satisfying the coherence condition already discussed for structural bimodules and, in addition, two extra coherence conditions: the following and its dual for δ_{R}^{L}.

[figure: (X ⦸ Y) ⊘ F (A); δ_{L}^{R}; (X ⊘ F (A)) ⦸ Y; θ; θ ⦸ 1; F ((X ⦸ Y) ⊘ A); F (δ_{L}^{R}); F ((X ⊘ A) ⦸ Y); ϕ; F (X ⊘ A) ⦸ Y]

A natural transformation is bistrong in case it is both (contextually) strong and (cocontextually) costrong. The reader may check that bicontext bimodules, bistrong functors and bistrong transformations form a 2–category.

Now to complete the definition of a bicontext category we require that all the functors and transformations be bistrong. In fact, by requiring the category to be both context and cocontext, we already have that the transformations associated with ⊘ are strong and that those related to ⦸ are costrong. The coherence conditions which remain are those which assert the costrength of ⊘ , the strength of ⦸ , the costrength of the ⊘ related transformations, and the strength of the ⦸ related transformations. In all these the cut distributions play an important role. We shall illustrate some of these diagrams, leaving an enumeration to a sequel, although the recipe given already suffices to allow the reader to generate such an enumeration.

Using Proposition 2.9 we may express the strength of ⦸ in terms of the cut distributions. However, this implies the requirement that the following diagram commutes (likewise its dual involving δ_{L}^{R} whose equation we provide):

[figure: X ⊘ (Y ⊘ (A ⦸ B)); 1 ⊘ δ_{R}^{L}; X ⊘ (A ⦸ (Y ⊘ B)); c_{⊘}; δ_{L}^{L}; Y ⊘ (X ⊘ (A ⦸ B)); 1⊘δ_{L}^{L}; Y ⊘ ((X ⊘ A) ⦸ B); δ_{R}^{L}; (X ⊘ A) ⦸ (Y ⊘ B)]

1 ⊘ δ_{R}^{L}; δ_{L}^{L} = c_{⊘}; 1 ⊘ δ_{L}^{L}; δ_{R}^{L}  (28)
δ_{L}^{L}; δ_{L}^{R} ⦸ 1 = δ_{L}^{R}; δ_{L}^{L} ⦸ 1; c_{⦸}  (29)

Finally we have to add coherence diagrams which arise from the requirement that the transformations bistrong. We shall illustrate these with one example: the requirement that b be strong. One requirement (equation (27)) has already been described, as this arises in structural bimodules. The additional requirement arises from moving the context onto the second argument, which only makes sense for bicontext bimodules. Explicitly it is that the following diagram commutes:

[figure: X ⊘ ((Y ⦸ Z) ⦸ Z); 1 ⊘ b; X ⊘ (Y ⦸ Z); d; X ⊘ (X ⊘ ((Y ⦸ Z) ⦸ Z)); 1 ⊘ δ_{R}^{L}; X ⊘ ((Y ⦸ Z) ⦸ (X ⊘ Z)); δ_{R}^{L}; δ_{L}^{L}; (X ⊘ (Y ⦸ Z)) ⦸ (X ⊘ Z); δ_{R}^{L} ⦸ 1; (Y ⦸ (X ⊘ Z)) ⦸ (X ⊘ Z); b; Y ⦸ (X ⊘ Z)]

1 ⊘ b; δ_{R}^{L} = d; 1 ⊘ δ_{R}^{L}; δ_{L}^{L}; δ_{R}^{L}; b  (30)

3.6 Bicontextual weakly distributive categories The final additional structure considered in this paper is that of a tensor and cotensor (“par”). This, in greatest generality, will give a weakly distributive (X, Z)–bicontextual bimodule Y. From the fibrational view, this is a weakly distributive category in the 2-category of fibrational forks. We shall concentrate as above, however, on the case X = Y = Z to obtain a bicontextual weakly distributive category.

It should be pointed out that one can add in a modular fashion the further operators of linear logic to the basic structure of a weakly distributive category. This is described in our previous papers [CS91, BCST, BCS92, CS96]. Thus we may also build, in a modular fashion, on bicontextual weakly distributive categories to interpret other structure associated with linear logic settings. For example, one may add negation to obtain a bicontextual ∗-autonomous category by following the recipe in [CS91]. Thus, the structure we outline here provides the heart of the matter, and avoids excessive use of symmetry, negation, or closed structure.

We have already seen, in subsection 2.4, how to add a contextually strong tensor product ⊗. But we should remind the reader of an issue we mentioned then: namely whether we want the single argument (or linear) strengths fst and snd for the tensor to be isomorphisms. We saw that this requirement will lead us to a system that is essentially the usual ⊗– ! logic. Similarly when cocontext and cotensor are added, this will lead to the full strength of weakly distributive categories with storage, in short, to the tensor-par- ! - ? fragment of linear logic. However, from the point of view of this paper, from a strength-driven perspective, this requirement is not necessary nor indeed particularly natural. Despite this, from now on we will give more emphasis to the more familiar logic which is a fragment of Girard’s system. We think that the more general system is of significant interest, and probably in the long run of greater importance, so we shall point out as we proceed the changes necessary to obtain the more general system.

This means we must have these linear strength maps:

fst_{⊗} = θ _{⊗Z}: X ⊘ (Y ⊗ Z) ⟶ (X ⊘ Y) ⊗ Z
snd_{⊗} = θ_{Y ⊗} : X ⊘ (Y ⊗ Z) ⟶ Y ⊗ (X ⊘ Z)

together with their inverses

fst−1_{⊗}: (X ⊘ Y) ⊗ Z ⟶ X ⊘ (Y ⊗ Z)
snd−1_{⊗}: Y ⊗ (X ⊘ Z) ⟶ X ⊘ (Y ⊗ Z)

As before, we require that ⊗ be strong, but in addition it must be costrong (with respect to ⦸), which gives two more natural transformations ϕ_{⊤}, ϕ_{⊗}, as well as the induced fst′_{⊗}, snd′_{⊗}, as listed in Table 1, and we require that ⊗ be bistrong, which imposes more coherence conditions.

Next we add the cotensor (or “par”) ⊕; of course we then require that ⊕ be bistrong, giving morphisms and diagrams dual to those above. In addition, we shall require that ⊗, ⊕ have the structure of a weakly distributive category, adding the appropriate distributivities and commuting diagrams. Furthermore, the weak distributivities must be bistrong.

At this point, it seems worthwhile to summarize all the natural transformations we have required; these may be found in Table 1. Of course, the various coherence conditions must be added, as outlined so far in this paper.

d: X ⊘ Y ⟶ X ⊘ (X ⊘ Y)  b: (X ⦸ Y) ⦸ Y ⟶ X ⦸ Y
e: X ⊘ Y ⟶ Y  i: X ⟶ X ⦸ Y
a_{⊘}: X ⊘ (Y ⊘ Z) ⟶ (X ⊘ Y) ⊘ Z  a_{⦸}: X ⦸ (Y ⦸ Z) ⟶ (X ⦸ Y) ⦸ Z
c_{⊘}: X ⊘ (Y ⊘ Z) ⟶ Y ⊘ (X ⊘ Z)  c_{⦸}: (X ⦸ Y) ⦸ Z ⟶ (X ⦸ Z) ⦸ Y
lift: X ⟶ ⊤ ⊘ X  colift: X ⦸ ⊥ ⟶ X
read: X ⊘ ⊤ ⟶ X  coread: X ⟶ ⊥ ⦸ X
δ_{L}^{L}: X ⊘ (Y ⦸ Z) ⟶ (X ⊘ Y) ⦸ Z
δ_{R}^{L}: X ⊘ (Y ⦸ Z) ⟶ Y ⦸ (X ⊘ Z)
δ_{L}^{R}: (X ⦸ Y) ⊘ Z ⟶ (X ⊘ Z) ⦸ Y
θ_{⊤}: X ⊘ ⊤ ⟶ ⊤  θ_{⊥}: ⊥ ⟶ ⊥ ⦸ X
θ_{⊗}: X ⊘ (A ⊗ B) ⟶ (X ⊘ A) ⊗ (X ⊘ B)  θ_{⊕}: (A ⦸ X) ⊕ (B ⦸ X) ⟶ (A ⊕ B) ⦸ X
fst_{⊗}: X ⊘ (A ⊗ B) ⟶ (X ⊘ A) ⊗ B  fst_{⊕}: A ⊕ (B ⦸ X) ⟶ (A ⊕ B) ⦸ X
snd_{⊗}: X ⊘ (A ⊗ B) ⟶ A ⊗ (X ⊘ B)  snd_{⊕}: (A ⦸ X) ⊕ B ⟶ (A ⊕ B) ⦸ X
fst−1_{⊗}: (X ⊘ A) ⊗ B ⟶ X ⊘ (A ⊗ B)  fst−1_{⊕}: (A ⊕ B) ⦸ X ⟶ A ⊕ (B ⦸ X)
snd−1_{⊗}: A ⊗ (X ⊘ B) ⟶ X ⊘ (A ⊗ B)  snd−1_{⊕}: (A ⊕ B) ⦸ X ⟶ (A ⦸ X) ⊕ B
ϕ_{⊥}: X ⊘ ⊥ ⟶ ⊥  ϕ_{⊤}: ⊤ ⟶ ⊤ ⦸ X
ϕ_{⊕}: X ⊘ (A ⊕ B) ⟶ (X ⊘ A) ⊕ (X ⊘ B)  ϕ_{⊗}: (A ⦸ X) ⊗ (B ⦸ X) ⟶ (A ⊗ B) ⦸ X
fst′_{⊕}: X ⊘ (A ⊕ B) ⟶ (X ⊘ A) ⊕ B  fst′_{⊗}: A ⊗ (B ⦸ X) ⟶ (A ⊗ B) ⦸ X
snd′_{⊕}: X ⊘ (A ⊕ B) ⟶ A ⊕ (X ⊘ B)  snd′_{⊗}: (A ⦸ X) ⊗ B ⟶ (A ⊗ B) ⦸ X
∂: X ⊗ (Y ⊕ Z) ⟶ (X ⊗ Y) ⊕ Z
∂′: (X ⊕ Y) ⊗ Z ⟶ X ⊕ (Y ⊗ Z)
a_{⊗}: X ⊗ (Y ⊗ Z) ⟶^{∼} (X ⊗ Y) ⊗ Z  a_{⊕}: X ⊕ (Y ⊕ Z) ⟶^{∼} (X ⊕ Y) ⊕ Z
uR_{⊗}: A ⊗ ⊤ ⟶^{∼} A  uR_{⊕}: A ⊕ ⊥ ⟶^{∼} A
uL_{⊗}: ⊤ ⊗ A ⟶^{∼} A  uL_{⊕}: ⊥ ⊕ A ⟶^{∼} A

Table 1: Summary of required natural transformations

Remark 3.7 (Equivalence to ! and ? ) It seems quite clear to us that the doctrine of bicontextual weakly distributive categories (as defined above, with isomorphisms for the strength of tensor and the costrength of cotensor) is equivalent to the doctrine of weakly distributive categories with storage [BCS92]. As with our conjecture concerning MELL, the only obstacle to verifying this is the number of diagrams that must be checked, each involving a routine diagram-chase. What is obvious is that the two constructions, of ! and ? from ⊘ and ⦸, and vice versa, are inverse. However, there are numerous coherence conditions to be checked and we are content, in this paper, to leave this as a conjecture. The main objective has been to describe the construction of the setting from the perspective of strength. We do intend to return to these issues in a sequel when the proof circuits are introduced. □

4 The context calculus

It must be obvious by now that the structures we have been studying are very similar to Girard’s approach to unifying classical and linear logic [G93]: context and cocontext variables are “classical” and general variables are “linear”. This is represented by a morphism C ⊘G ⟶ H ⦸D; the position C before the ⊘ is “classical”, while the position G after ⊘ is “linear”; dually, the H before the ⦸ is “linear” and the D after is “classical”. In the remainder of this paper we shall develop this idea, representing it by sequents Γ; Π ⊢ Σ; Δ, where Γ, Π, Σ, Δ are finite (including possibly empty) sequences of formulas. Note that in a sense the role of ⊘, ⦸ is taken by the semicolon in the sequent, before or after the turnstile, as appropriate. We shall present the sequent calculus, outline the cut elimination theorem for it, and sketch the interpretation of the calculus in context categories.

4.1 Sequent rules We begin with the sequent calculus—as suggested above, this is a fragment of unified logic, and is intended to illustrate the way in which context categories handle the features of ! and ? , and how they handle the interaction of classical and linear behaviour. The sequent rules are listed in Tables 2, 3.^{4}

There are some subtleties we should discuss before proceeding to the categorical definitions. The structure rules are fairly straightforward—the “classical” rules of contraction, thinning, and exchange are restricted to the “classical” part of the sequent. Dereliction allows a formula used “linearly” to move into the “classical” part of the sequent.

The three cut rules correspond to the strengths and costrengths of each action over the other, that is, to the δ transformations. Consider these instances of the various types of cut:

\begin{matrix}; Y ⦸ Z ⊢ Y; Z & X; Y ⊢ X ⊘ Y; \\ X; Y ⦸ Z ⊢ X ⊘ Y; Z \end{matrix} (llcut)

\begin{matrix}; Y ⦸ Z ⊢ Y; Z & X; Z ⊢ X ⊘ Z; \\ X; Y ⦸ Z ⊢ Y; X ⊘ Z \end{matrix} (clcut)
\begin{matrix}; X ⦸ Y ⊢ X; Y & X; Z ⊢ X ⊘ Z; \\ X ⦸ Y; Z ⊢ X ⊘ Z; Y \end{matrix} (lccut)

Now, A; B ⊢ A ⊘ B; is easily derivable^{5} using (⊘ R) and ; A ⦸ B ⊢ A; B is easily derivable using (⦸ L). So the three derivations above yield the three δ transformations

δ_{L}^{L}: X ⊘ (Y ⦸ Z) ⊢ (X ⊘ Y) ⦸ Z
δ_{R}^{L}: X ⊘ (Y ⦸ Z) ⊢ Y ⦸ (X ⊘ Z)
δ_{L}^{R}: (X ⦸ Y) ⊘ Z ⊢ (X ⊘ Z) ⦸ Y

The (llcut) rule has the usual “planarity” condition, as in [CS91] for instance. We can relax this condition, at the cost of introducing some dereliction; the variants (lLcut) and (Llcut) are the Axioms:

4We call this “the context calculus”, a shorter name than “the bicontextual weakly distributive calculus”.

5More generally, the reader can readily derive X_{1}, …, X_{n}; Y_{1}, …, Y_{m} ⊢ X_{1} ⊘ (⋯ ⊘ (X_{n} ⊘ (Y_{1} ⊗ (⋯ ⊗ Y_{m})))); and its dual.

; A ⊢ A; (id)

Structure Rules:

Γ, A, A, Γ′; Π ⊢ Σ; Δ Γ, A, Γ′; Π ⊢ Σ; Δ (⊘ contr)  Γ; Π ⊢ Σ; Δ, A, A, Δ′ Γ; Π ⊢ Σ; Δ, A, Δ′ (⦸ contr)

Γ, Γ′; Π ⊢ Σ; Δ Γ, A, Γ′; Π ⊢ Σ; Δ (⊘ thin)  Γ; Π ⊢ Σ; Δ, Δ′ Γ; Π ⊢ Σ; Δ, A, Δ′ (⦸ thin)

Γ, A, B, Γ′; Π ⊢ Σ; Δ Γ, B, A, Γ′; Π ⊢ Σ; Δ (⊘ exch)  Γ; Π ⊢ Σ; Δ, A, B, Δ′ Γ; Π ⊢ Σ; Δ, B, A, Δ′ (⦸ exch)

Γ; A, Π ⊢ Σ; Δ Γ, A; Π ⊢ Σ; Δ (⊘ der)  Γ; Π ⊢ Σ, A; Δ Γ; Π ⊢ Σ; A, Δ (⦸ der)

Cut rules:

Γ_{1}; Π_{1} ⊢ Σ_{1}, A, Σ′_{1}; Δ_{1}  Γ_{2}; Π_{2}, A, Π′_{2} ⊢ Σ_{2}; Δ_{2}

Γ_{2}, Γ_{1}; Π_{2}, Π_{1}, Π′_{2} ⊢ Σ_{1}, Σ_{2}, Σ′_{1}; Δ_{2}, Δ_{1} (llcut)^{†}

†where either Σ_{1} = ∅ or Π_{2} = ∅ and either Σ′_{1} = ∅ or Π′_{2} = ∅
Γ_{1}; Π_{1} ⊢ Σ_{1}, A, Σ′_{1}; Δ_{1}  Γ_{2}; Π_{2}, A, Π′_{2} ⊢ Σ_{2}; Δ_{2}

Γ_{2}, Π_{2}, Γ_{1}; Π_{1}, Π′_{2} ⊢ Σ_{1}, Σ_{2}, Σ′_{1}; Δ_{2}, Δ_{1} (lLcut)^{♭}

♭where Π_{2} ≠ ∅ and either Σ′_{1} = ∅ or Π′_{2} = ∅
Γ_{1}; Π_{1} ⊢ Σ_{1}, A, Σ′_{1}; Δ_{1}  Γ_{2}; Π_{2}, A, Π′_{2} ⊢ Σ_{2}; Δ_{2}

Γ_{2}, Γ_{1}; Π_{2}, Π_{1}, Π′_{2} ⊢ Σ_{1}, Σ_{2}; Δ_{2}, Σ′_{1}, Δ_{1} (Llcut)^{♯}

♯where Σ′_{1} ≠ ∅ and either Σ_{1} = ∅ or Π_{2} = ∅
Γ_{1}; Π_{1} ⊢ Σ_{1}; Δ_{1}, A, Δ′_{1}  Γ_{2}; Π_{2}, A ⊢ Σ_{2}; Δ_{2}

Γ_{2}, Π_{2}, Γ_{1}; Π_{1} ⊢ Σ_{1}; Δ_{1}, Σ_{2}, Δ_{2}, Δ′_{1} (clcut)

Γ_{1}; Π_{1} ⊢ A, Σ_{1}; Δ_{1}  Γ_{2}, A, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}

Γ_{2}, Γ_{1}, Π_{1}, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}, Σ_{1}, Δ_{1} (lccut)

Table 2: Sequent rules for the context calculus – I

results. These rules may be derived, but for the purposes of cut elimination it is convenient to include them as bona fide rules in their own right. In the “mixed” cuts, (lccut), (clcut), we have also built in some instances of dereliction, which gives them an apparently greater generality than Unit Rules:

Γ; Π, Π′ ⊢ Σ; Δ Γ; Π, ⊤, Π′ ⊢ Σ; Δ (⊤ L)  ; ⊢ ⊤; (⊤ R)

; ⊥ ⊢ ; (⊥ L)  Γ; Π ⊢ Σ, Σ′; Δ Γ; Π ⊢ Σ, ⊥, Σ′; Δ (⊥ R)

Context Rules:

Γ, A; Π, B, Π′ ⊢ Σ; Δ Γ; Π, A ⊘ B, Π′ ⊢ Σ; Δ (⊘ L)  Γ_{1}; Π_{1} ⊢ A; Δ_{1} Γ_{2}; Π_{2} ⊢ Σ_{2}, B, Σ′_{2}; Δ_{2} Γ_{1}, Π_{1}, Γ_{2}; Π_{2} ⊢ Σ_{2}, A ⊘ B, Σ′_{2}; Δ_{1}, Δ_{2} (⊘ R)

Γ_{1}; Π_{1}, A, Π′_{1} ⊢ Σ_{1}; Δ_{1} Γ_{2}; B ⊢ Σ_{2}; Δ_{2} Γ_{1}, Γ_{2}; Π_{1}, A ⦸ B, Π′_{1} ⊢ Σ_{1}; Δ_{1}, Σ_{2}, Δ_{2} (⦸ L)  Γ; Π ⊢ Σ, A, Σ′; B, Δ Γ; Π ⊢ Σ, A ⦸ B, Σ′; Δ (⦸ R)

Tensor Rules:

Γ; Π, A, B, Π′ ⊢ Σ; Δ Γ; Π, A ⊗ B, Π′ ⊢ Σ; Δ (⊗ L)  Γ_{1}; Π_{1} ⊢ Σ_{1}, A; Δ_{1} Γ_{2}; Π_{2} ⊢ B, Σ_{2}; Δ_{2} Γ_{1}, Γ_{2}; Π_{1}, Π_{2} ⊢ Σ_{1}, A ⊗ B, Σ_{2}; Δ_{1}, Δ_{2} (⊗ R)

Γ_{1}; Π_{1}, A ⊢ Σ_{1}; Δ_{1} Γ_{2}; B, Π_{2} ⊢ Σ_{2}; Δ_{2} Γ_{1}, Γ_{2}; Π_{1}, A ⊕ B, Π_{2} ⊢ Σ_{1}, Σ_{2}; Δ_{1}, Δ_{2} (⊕ L)  Γ; Π ⊢ Σ, A, B, Σ′; Δ Γ; Π ⊢ Σ, A ⊕ B, Σ′; Δ (⊕ R)

Table 3: Sequent rules for the context calculus – II

the corresponding rules given by Girard. One can easily check they are equivalent; however, in these two “mixed” cut rules there is a crucial use of this dereliction in deriving δ_{R}^{L}, δ_{L}^{R}, as may be verified above. As we are taking strength as our primary notion in this paper, these versions of cut seem more appropriate.

There is a “missing” (cccut) rule, both in our system and in Girard’s, corresponding to the “missing” δ_{R}^{R} distributivity mentioned above.

Next we shall consider the (⊘ L) rule. In the form presented here, this rule is equivalent (in the presence of the cut rules) to the following axioms, corresponding to the inverses of the linear strengths of ⊗:

(X ⊘ Y) ⊗ Z ⊢ X ⊘ (Y ⊗ Z)
Y ⊗ (X ⊘ Z) ⊢ X ⊘ (Y ⊗ Z)

If we took the path of not requiring these inverses in our categorical semantics, then we would have to content ourselves with a much more restricted (⊘ L) rule:

{Γ, A; B ⊢ Σ; Δ \atop Γ; A ⊘ B ⊢ Σ; Δ} (⊘ l)

Similar remarks apply to (⦸ R), where dropping the inverses to fst_{⊕}, snd_{⊕} would require a restricted sequent rule.

The linear strengths of ⊗, viz. the “inverses” of these axioms, are also derivable, using (llcut). We shall illustrate this with these instances of (llcut):

\begin{matrix}X; Z ⊢ X ⊘ Z; & Γ; Y, X ⊘ Z, Π ⊢ W; \\ Γ, X; Y, Z, Π ⊢ W; \end{matrix} (llcut)

\begin{matrix}X; Y ⊢ X ⊘ Y; & Γ; X ⊘ Y, Z, Π ⊢ W; \\ Γ, X; Y, Z, Π ⊢ W \end{matrix} (llcut)

Now, A; B ⊢ A ⊘ B; is derivable , so letting Γ, Π be empty, and making a suitable choice for W above will give the desired axioms:

X ⊘ (Y ⊗ Z) ⊢ (X ⊘ Y) ⊗ Z
X ⊘ (Y ⊗ Z) ⊢ Y ⊗ (X ⊘ Z)

More generally, we have this derived rule, which combines the two above:

{Γ; X ⊘ Y, X ⊘ Z, Π ⊢ W; \atop Γ, X; Y, Z, Π ⊢ W;}

which is easily proved thus:

\begin{aligned}X; Z ⊢ X ⊘ Z; & \begin{matrix}X; Y ⊢ X ⊘ Y; & Γ; X ⊘ Y, X ⊘ Z, Π ⊢ W; \\ Γ, X; Y, X ⊘ Z, Π ⊢ W; \end{matrix} (llcut) \\ & Γ, X, X; Y, Z, Π ⊢ W; \end{aligned} ; (llcut)

Γ, X; Y, Z, Π ⊢ W; (contr)

which induces the general strength transformation for ⊗:

X ⊘ (Y ⊗ Z) ⟶ (X ⊘ Y) ⊗ (X ⊘ Z)

The (⊘ R) rule has an essential instance of dereliction, at Π_{1}, which is necessary for the rule to be able to generate the sequent A; B ⊢ A ⊘ B; . We could add another instance of dereliction if needed, adding a Σ′_{1} after the A, but the form we have given seems most useful for our purposes. Note the role of the Σ_{2} however; it essentially expresses the strength of ⊕:

\begin{matrix}; A ⊢ A; & ; C ⊕ B ⊢ C, B; \\ A; C ⊕ B ⊢ C, A ⊘ B; \end{matrix} (⊘ R)

giving the entailment A ⊘ (C ⊕ B) ⟶ C ⊕ (A ⊘ B). Dually, the Σ′_{2} generates the other linear strength transformation of ⊕.

\begin{matrix}; A ⊢ A; & ; B ⊕ C ⊢ B, C; \\ A; B ⊕ C ⊢ A ⊘ B, C; \end{matrix} (⊘ R)

A corresponding Σ_{1} before the A would invoke a notion dual to the strength of ⊕, (an “opstrength”, as opposed to costrength) and so we do not have any such nonempty list in front of the A. Likewise an underelicted Σ′_{1} after the A is not desirable.

The costrengths of ⊕ and ⊗ explain the ⦸ rules in a dual manner.

The unit rules essentially amount to making the constant ⊤ carry the structure of an empty linear formula, that is, an empty formula after the semicolon on the left of the turnstile, and dually ⊥ corresponds to an empty linear formula on the right. In other words, the constants ⊤, ⊥ are the units for the ⊗, ⊕ respectively, which correspond to the “commas” in the linear part of the sequents. Note that ⊤ is not the unit for the ⊘, which would require a constant carrying the structure of an empty classical formula, that is, an empty formula before the semicolon, nor is ⊥ the unit for ⦸. The tensor rules are fairly self-explanatory, and agree with Girard’s rules in essence—we have merely been more careful not to assume symmetry in the “linear” parts of the sequent.

To summarize, all the structure we have imposed on our categorical semantics is supported by this sequent calculus. Proposition 4.1 Entailments corresponding to all the transformations of Table 1 are derivable in the context calculus. Proof (Sketch). Some of this has already been done above. We shall just illustrate the highlights of the remainder. d and b are given by contraction, e and i by thinning. a and c use the context rules; here is the key part of the derivation of c_{⊘} for example.

\begin{matrix}\begin{matrix}; Y ⊢ Y; & X; Z ⊢ X ⊘ Z; \\ Y, X; Z ⊢ Y ⊘ (X ⊘ Z) \end{matrix} & (⊘ R) \\ X, Y; Z ⊢ Y ⊘ (X ⊘ Z) \end{matrix} ; (⊘ exch) ; X; Y ⊘ Z ⊢ Y ⊘ (X ⊘ Z) ; (⊘ L)

read is given by thinning and dereliction; lift by a cut:

\begin{aligned}; ⊢ ⊤; & ⊤; X ⊢ ⊤ ⊘ X; \\ & ; X ⊢ ⊤ ⊘ X \end{aligned} (lccut)

and dually for coread and colift.

We have seen the δ’s and the θ’s above (θ_{⊤} is given by thinning), including fst, snd and their inverses. ϕ_{⊥} is given by thinning, and ϕ_{⊕} by (⊕ L) and (⊘ contr); the other ϕ’s are dual. The tensor weak distributivities are simple (llcut)’s; here is ∂ for example.

\begin{matrix}; Y ⊕ Z ⊢ Y, Z; & ; X, Y ⊢ X ⊗ Y; \\ ; X, Y ⊕ Z ⊢ X ⊗ Y, Z; \end{matrix} (llcut)

Finally, the tensor associativities follow from (⊗ R) and the tensor unit isomorphisms follow from the (⊤ L) rule; the cotensor isomorphisms are dual. □

4.2 Interpretation As we said above, we interpret a sequent G_{1}, …, G_{n}; P_{1}, …, P_{m} ⊢ S_{1}, …, S_{k}; D_{1}, …, D_{l} as a morphism G_{1} ⊘ (⋯ ⊘ (G_{n} ⊘ (P_{1} ⊗ (⋯ ⊗ P_{m})))) ⟶ ((S_{1} ⊕ (⋯ ⊕ S_{k}) ⦸ D_{1}) ⋯) ⦸ D_{l}. If a “classical” part of the sequent is empty, we just ignore the missing term, and if a “linear” part of the sequent is empty, we use the appropriate unit ⊤ or ⊥ in that position. So, e.g. ; P ⊢ ; D would be interpreted as a morphism P ⟶ ⊥ ⦸ D. In this way then, the (id) axiom is just the identity morphism A ⟶ A. The structure rules are given by the defining natural transformations for bicontext categories: for example, ⊘ contraction is induced by the duplication natural transformation d: X ⊘Y ⟶ X ⊘(X ⊘Y); ⊘ thinning is induced by the elimination natural transformation e: X ⊘Y ⟶ Y; ⊘ exchange is induced by c_{⊘}: X ⊘ (Y ⊘ Z) ⟶ Y ⊘ (X ⊘ Z); and ⊘ dereliction is induced by read: X ⊘ ⊤ ⟶ X. We illustrate this with an example of dereliction. First note that there is a derived natural transformation Δ: A ⊘ P ⟶ A ⊗ P, which is the essence of dereliction:

Δ: A ⊘ P ⟶^{1 ⊘ u^{−1}} A ⊘ (⊤ ⊗ P) ⟶^{fst_{⊗}} (A ⊘ ⊤) ⊗ P ⟶^{read ⊗1} A ⊗ P

Then, given f: G⊘(A⊗P) ⟶ W, we get the derelicted morphism G⊘(A⊘P) ⟶^{1 ⊘ Δ} G⊘(A⊗P)

⟶^{f} W.

The ⦸ rules are dual; generally we shall not refer to the ⦸ cases, leaving the reader to do the appropriate dualization. But we do draw attention to the transformation dual to Δ, namely ∇: A ⊕ X ⟶ A ⦸ X, ∇ = 1 ⊕ coread; fst_{⊕}; u_{⊕} ⦸ 1.

There are several cases of cut to verify. We shall illustrate (llcut), (lccut) with the derelictions, but shall take a shortcut for (clcut), dropping them. We leave (lLcut) and (Llcut) as exercises, since they may be derived from (llcut) and dereliction. In the following examples, we suppose the sequences in the cut rules are all single formulas; the reader can derive the nullary and n-ary cases. Suppose f: G_{1} ⊘ P_{1} ⟶ (A ⊕ S_{1}) ⦸ D_{1}, g: G_{2} ⊘ (P_{2} ⊗ A) ⟶ S_{2} ⦸ D_{2}, p: G_{1} ⊘ P_{1} ⟶ (S_{1} ⊕ A) ⦸ D_{1}, and q: G_{2} ⊘ (A ⊗ P_{2}) ⟶ S_{2} ⦸ D_{2}. Then (llcut)(f, g) is given as follows:

G_{2} ⊘ (G_{1} ⊘ (P_{2} ⊗ P_{1})) ⟶^{1 ⊘ snd_{⊗}} G_{2} ⊘ (P_{2} ⊗ (G_{1} ⊘ P_{1}))

⟶^{1 ⊘ (1 ⊗ f)} G_{2} ⊘ (P_{2} ⊗ ((A ⊕ S_{1}) ⦸ D_{1})) ⟶^{1 ⊘ fst′_{⊗}} G_{2} ⊘ ((P_{2} ⊗ (A ⊕ S_{1})) ⦸ D_{1})

⟶^{δ_{L}^{L}} (G_{2} ⊘ (P_{2} ⊗ (A ⊕ S_{1}))) ⦸ D_{1} ⟶^{(1 ⊘ ∂) ⦸ 1} (G_{2} ⊘ ((P_{2} ⊗ A) ⊕ S_{1})) ⦸ D_{1}

⟶^{fst′_{⊕} ⦸1} ((G_{2} ⊘ (P_{2} ⊗ A)) ⊕ S_{1}) ⦸ D_{1} ⟶^{(g ⊕ 1) ⦸ 1} ((S_{2} ⦸ D_{2}) ⊕ S_{1}) ⦸ D_{1}

⟶^{snd_{⊕} ⦸1} ((S_{2} ⊕ S_{1}) ⦸ D_{2}) ⦸ D_{1}

and (llcut)(p, q) is given as follows:

G_{2} ⊘ (G_{1} ⊘ (P_{1} ⊗ P_{2})) ⟶^{1 ⊘ fst_{⊗}} G_{2} ⊘ ((G_{1} ⊘ P_{1}) ⊗ P_{2})

⟶^{1 ⊘ (p ⊗ 1)} G_{2} ⊘ (((S_{1} ⊕ A) ⦸ D_{1}) ⊗ P_{2}) ⟶^{1 ⊘ snd′_{⊗}} G_{2} ⊘ (((S_{1} ⊕ A) ⊗ P_{2}) ⦸ D_{1})

⟶^{1 ⊘ (∂′ ⦸ 1)} G_{2} ⊘ ((S_{1} ⊕ (A ⊗ P_{2})) ⦸ D_{1}) ⟶^{δ_{L}^{L}} (G_{2} ⊘ (S_{1} ⊕ (A ⊗ P_{2}))) ⦸ D_{1}

⟶^{snd′_{⊕} ⦸1} (S_{1} ⊕ (G_{2} ⊘ (A ⊗ P_{2}))) ⦸ D_{1} ⟶^{(1 ⊕ q) ⦸ 1} (S_{1} ⊕ (S_{2} ⦸ D_{2})) ⦸ D_{1}

⟶^{fst_{⊕} ⦸1} ((S_{1} ⊕ S_{2}) ⦸ D_{2}) ⦸ D_{1}

Next, given f: G_{1} ⊘ P_{1} ⟶ (A ⊕ S_{1}) ⦸ D_{1} and g: G_{2} ⊘ (A ⊘ (G′_{2} ⊘ P_{2})) ⟶ S_{2} ⦸ D_{2}, then (lccut)(f, g) is given as:

G_{2} ⊘ (G_{1} ⊘ (P_{1} ⊘ (G′_{2} ⊘ P_{2}))) ⟶^{1 ⊘ a_{⊘}} G_{2} ⊘ ((G_{1} ⊘ P_{1}) ⊘ (G′_{2} ⊘ P_{2}))

⟶^{1 ⊘ (f ⊘ 1)} G_{2} ⊘ (((A ⊕ S_{1}) ⦸ D_{1}) ⊘ (G′_{2} ⊘ P_{2}))

⟶^{1 ⊘ ((∇ ⦸ 1) ⊘ 1)} G_{2} ⊘ (((A ⦸ S_{1}) ⦸ D_{1}) ⊘ (G′_{2} ⊘ P_{2}))

⟶^{1 ⊘ δ_{L}^{R}} G_{2} ⊘ (((A ⦸ S_{1}) ⊘ (G′_{2} ⊘ P_{2})) ⦸ D_{1})

⟶^{1 ⊘ (δ_{L}^{R} ⦸ 1)} G_{2} ⊘ (((A ⊘ (G′_{2} ⊘ P_{2})) ⦸ S_{1}) ⦸ D_{1})

⟶^{δ_{L}^{L}} (G_{2} ⊘ ((A ⊘ (G′_{2} ⊘ P_{2})) ⦸ S_{1})) ⦸ D_{1}

⟶^{δ_{L}^{L} ⦸ 1} ((G_{2} ⊘ (A ⊘ (G′_{2} ⊘ P_{2}))) ⦸ S_{1}) ⦸ D_{1}

⟶^{(g ⦸ 1) ⦸ 1} ((S_{2} ⦸ D_{2}) ⦸ S_{1}) ⦸ D_{1}

The handling of dereliction for (clcut) is similar, so we illustrate (clcut) with a dereliction-free case, essentially the cut rule as Girard gives it. Suppose f: G_{1} ⊘ P ⟶ (S ⦸ A) ⦸ D_{1} and g: G_{2} ⊘ A ⟶ D_{2}. Then (clcut)(f, g) is

\begin{matrix}G_{2} ⊘ (G_{1} ⊘ P) ⟶^{1 ⊘ f} G_{2} ⊘ ((S ⦸ A) ⦸ D_{1} ⟶^{δ_{L}^{L}} (G_{2} ⊘ (S ⦸ A)) ⦸ D_{1} \\ ⟶^{δ_{R}^{L} ⦸ 1} (S ⦸ (G_{2} ⊘ A)) ⦸ D_{1} ⟶^{(1 ⦸ g) ⦸ 1} (S ⦸ D_{2}) ⦸ D_{1} \end{matrix}

The unit rules are trivial, and the reader may easily verify the claim made earlier that (⊘ L) is induced by fst−1_{⊗} and snd−1_{⊗}. The restricted (⊘ l) rule (suitable in a calculus for the semantics where we do not require the linear tensor strengths fst and snd to be isomorphisms) is trivial; the conclusion has the same interpretation as the premise.

To interpret (⊘ R), suppose we are given f: G_{1} ⊘ P_{1} ⟶ A ⦸ D_{1} and g: G_{2} ⊘ P_{2} ⟶ ((S_{2} ⊕ B) ⊕ S′_{2}) ⦸ D_{2}; then (⊘ R)(f, g) is

G_{1} ⊘ (P_{1} ⊘ (G_{2} ⊘ P_{2})) ⟶^{a_{⊘}} (G_{1} ⊘ P_{1}) ⊘ (G_{2} ⊘ P_{2})

⟶^{f ⊘ g} (A ⦸ D_{1}) ⊘ (((S_{2} ⊕ B) ⊕ S′_{2}) ⦸ D_{2})

⟶^{δ_{L}^{R}} (A ⊘ (((S_{2} ⊕ B) ⊕ S′_{2}) ⦸ D_{2})) ⦸ D_{1}

⟶^{δ_{L}^{L} ⦸ 1} ((A ⊘ ((S_{2} ⊕ B) ⊕ S′_{2})) ⦸ D_{2}) ⦸ D_{1}

⟶^{((1 ⊘ a_{⊕}) ⦸ 1) ⦸ 1} ((A ⊘ (S_{2} ⊕ (B ⊕ S′_{2}))) ⦸ D_{2}) ⦸ D_{1}

⟶^{(snd′_{⊕} ⦸1) ⦸ 1} ((S_{2} ⊕ (A ⊘ (B ⊕ S′_{2}))) ⦸ D_{2}) ⦸ D_{1}

⟶^{((1 ⊕ fst′_{⊕}) ⦸ 1) ⦸ 1} ((S_{2} ⊕ ((A ⊘ B) ⊕ S′_{2})) ⦸ D_{2}) ⦸ D_{1}

⟶^{(a_{⊕} ⦸ 1) ⦸ 1} (((S_{2} ⊕ (A ⊘ B)) ⊕ S′_{2}) ⦸ D_{2}) ⦸ D_{1}

The tensor rule (⊗ L) is just a matter of tensor associativity; the rule (⊗ R) involves composites much like those we have seen above, to move the pieces into the right places. But just as (⊘ R) essentially is just the functoriality of ⊘, so too is (⊗ R) essentially the functoriality of ⊗. Suppose f: G_{1} ⊘ P_{1} ⟶ (S ⊕ A) ⦸ D_{1} and g: G_{2} ⊘ P_{2} ⟶ (B ⊕ S_{2}) ⦸ D_{2}; then (⊗ R)(f, g) is

G_{1} ⊘ (G_{2} ⊘ (P_{1} ⊗ P_{2})) ⟶^{1 ⊘ snd_{⊗}} G_{1} ⊘ (P_{1} ⊗ (G_{2} ⊘ P_{2}))

⟶^{fst_{⊗}} (G_{1} ⊘ P_{1}) ⊗ (G_{2} ⊘ P_{2})

⟶^{f ⊗ g} ((S ⊕ A) ⦸ D_{1}) ⊗ ((B ⊕ S_{2}) ⦸ D_{2})

⟶^{fst′_{⊗}} (((S ⊕ A) ⦸ D_{1}) ⊗ (B ⊕ S_{2})) ⦸ D_{2}

⟶^{snd′_{⊗} ⦸1} ((S ⊕ A) ⊗ (B ⊕ S_{2})) ⦸ D_{1}) ⦸ D_{2}

⟶^{(∂′ ⦸ 1) ⦸ 1} ((S ⊕ (A ⊗ (B ⊕ S_{2}))) ⦸ D_{1}) ⦸ D_{2}

⟶^{((1 ⊕ ∂′) ⦸ 1) ⦸ 1} ((S ⊕ ((A ⊗ B) ⊕ S_{2})) ⦸ D_{1}) ⦸ D_{2}

4.3 Cut elimination The context calculus admits cut elimination; indeed the cut elimination process is quite straightforward. For the most part, the only interesting cases in the usual induction occur when the cut formula is the formula introduced by either one of or both of the rules that produce the premises of the cut. The other cases involve a routine permutation of the cut. We shall illustrate a representative sample of the induction steps here.

• (Permuting (llcut) and (⊘ contr)): In this case, the cut formula cannot be the formula contracted, so this is a case where a simple permutation of the contraction past the cut is all that is required. We shall illustrate this in both the case where the contraction appears in the left premise of the cut, and the case where it appears on the right.

Γ_{1}, A, A, Γ′_{1}; Π_{1} ⊢ Σ_{1}, B, Σ′_{1}; Δ_{1} Γ_{1}, A, Γ′_{1}; Π_{1} ⊢ Σ_{1}, B, Σ′_{1}; Δ_{1} Γ_{2}; Π_{2}, B, Π′_{2} ⊢ Σ_{2}; Δ_{2}

Γ_{2}, Γ_{1}, A, Γ′_{1}; Π_{2}, Π_{1}, Π′_{2} ⊢ Σ_{1}, Σ_{2}, Σ′_{1}; Δ_{2}, Δ_{1}

⟹

Γ_{1}, A, A, Γ′_{1}; Π_{1} ⊢ Σ_{1}, B, Σ′_{1}; Δ_{1} Γ_{2}; Π_{2}, B, Π′_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, Γ_{1}, A, A, Γ′_{1}; Π_{2}, Π_{1}, Π′_{2} ⊢ Σ_{1}, Σ_{2}, Σ′_{1}; Δ_{2}, Δ_{1}
Γ_{2}, Γ_{1}, A, Γ′_{1}; Π_{2}, Π_{1}, Π′_{2} ⊢ Σ_{1}, Σ_{2}, Σ′_{1}; Δ_{2}, Δ_{1}

Γ_{1}; Π_{1} ⊢ Σ_{1}, B, Σ′_{1}; Δ_{1}

Γ_{2}, A, A, Γ′_{2}; Π_{2}, B, Π′_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, A, Γ′_{2}; Π_{2}, B, Π′_{2} ⊢ Σ_{2}; Δ_{2}

Γ_{2}, A, Γ′_{2}, Γ_{1}; Π_{2}, Π_{1}, Π′_{2} ⊢ Σ_{1}, Σ_{2}, Σ′_{1}; Δ_{2}, Δ_{1}

⟹

Γ_{1}; Π_{1} ⊢ Σ_{1}, B, Σ′_{1}; Δ_{1} Γ_{2}, A, A, Γ′_{2}; Π_{2}, B, Π′_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, A, A, Γ′_{2}, Γ_{1}; Π_{2}, Π_{1}, Π′_{2} ⊢ Σ_{1}, Σ_{2}, Σ′_{1}; Δ_{2}, Δ_{1}
Γ_{2}, A, Γ′_{2}, Γ_{1}; Π_{2}, Π_{1}, Π′_{2} ⊢ Σ_{1}, Σ_{2}, Σ′_{1}; Δ_{2}, Δ_{1}

• (Permuting (lccut) and (⊘ contr)): The only cases where the contracted formula may be the cut formula occur when a (⊘ contr) appears on the right of a (lccut), and the dual case where a (⦸ contr) appears on the left of a (clcut). We illustrate the former; note that permuting the contraction introduces a second cut, higher up. Note also the use of numerous instances of exchange and contraction indicated by the double lines.

Γ_{1}; Π_{1} ⊢ A, Σ_{1}; Δ_{1}

Γ_{2}, A, A, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, A, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, Γ_{1}, Π_{1}, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}, Σ_{1}, Δ_{1}

⟹

Γ_{1}; Π_{1} ⊢ A, Σ_{1}; Δ_{1}

Γ_{1}; Π_{1} ⊢ A, Σ_{1}; Δ_{1} Γ_{2}, A, A, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, Γ_{1}, Π_{1}, A, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}, Σ_{1}, Δ_{1}
Γ_{2}, Γ_{1}, Π_{1}, Γ_{1}, Π_{1}, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}, Σ_{1}, Δ_{1}, Σ_{1}, Δ_{1}
Γ_{2}, Γ_{1}, Π_{1}, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}, Σ_{1}, Δ_{1}

• (Permuting (lccut) and (⊘ thin)): Again, the only interesting case is when the cut formula is introduced by thinning, which can only occur with (lccut) and (⊘ thin) or its dual (clcut) and (⦸ thin); we illustrate the former. Note the use of numerous instances of thinning indicated by the double line.

Γ_{1}; Π_{1} ⊢ A, Σ_{1}; Δ_{1}

Γ_{2}, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, A, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, Γ_{1}, Π_{1}, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}, Σ_{1}, Δ_{1}

⟹

Γ_{2}, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, Γ_{1}, Π_{1}, Γ′_{2}; Π_{2} ⊢ Σ_{2}; Δ_{2}, Σ_{1}, Δ_{1}

• (Permuting cuts and (exch)): These cases are completely analogous to the cases above.

• (Permuting (llcut) and (⊘ der)): This case is almost a straightforward permutation; the only case that is notable is when a possible violation of the “planarity” condition forces us to use a (lLcut) instead. For example

Γ_{1}; Π_{1} ⊢ Σ_{1}, B; Δ_{1}

Γ_{2}; A, B, Π_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, A; B, Π_{2} ⊢ Σ_{2}; Δ_{2}

Γ_{2}, A, Γ_{1}; Π_{1}, Π_{2} ⊢ Σ_{1}, Σ_{2}; Δ_{2}, Δ_{1}

⟹ Γ_{1}; Π_{1} ⊢ Σ_{1}, B; Δ_{1} Γ_{2}; A, B, Π_{2} ⊢ Σ_{2}; Δ_{2}

Γ_{2}, A, Γ_{1}; Π_{1}, Π_{2} ⊢ Σ_{1}, Σ_{2}; Δ_{2}, Δ_{1}

Note the point here is that the planarity restriction would be violated if we just did a standard permutation of the cut above the dereliction, so instead we use a (lLcut) which has the dereliction built in. If the planarity restriction is not violated by permuting the cut above the dereliction this would not be necessary.

• (Permuting (lccut) and (⊘ der)): Here is an example where the cut formula is the derelicted formula; note again the use of an (Llcut) in the rewrite to avoid a violation of the planarity condition; note also the numerous instances of dereliction indicated by the double line.

Γ_{1}; Π_{1} ⊢ A, Σ_{1}; Δ_{1}

Γ_{2}; A, Π_{2} ⊢ Σ_{2}; Δ_{2} Γ_{2}, A; Π_{2} ⊢ Σ_{2}; Δ_{2}

Γ_{2}, Γ_{1}, Π_{1}; Π_{2} ⊢ Σ_{2}; Δ_{2}, Σ_{1}, Δ_{1}

⟹

Γ_{1}; Π_{1} ⊢ A, Σ_{1}; Δ_{1} Γ_{2}; A, Π_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, Γ_{1}; Π_{1}, Π_{2} ⊢ Σ_{2}; Δ_{2}, Σ_{1}, Δ_{1}
Γ_{2}, Γ_{1}, Π_{1}; Π_{2} ⊢ Σ_{2}; Δ_{2}, Σ_{1}, Δ_{1}

• (Permuting (llcut) and ⊤): The interesting case is when ⊤ is the cut formula, introduced on both sides by the ⊤ rules. The ⊥ case is dual.

; ⊢ ⊤; Γ_{2}; Π_{2}, Π′_{2} ⊢ Σ_{2}; Δ_{2} Γ_{2}; Π_{2}, ⊤, Π′_{2} ⊢ Σ_{2}; Δ_{2} Γ_{2}; Π_{2}, Π′_{2} ⊢ Σ_{2}; Δ_{2}  ⟹  Γ_{2}; Π_{2}, Π′_{2} ⊢ Σ_{2}; Δ_{2}

• (Permuting (llcut) and ⊘): Again, the interesting case is when the operator introduced in the premises of the cut rule is the cut formula. We illustrate this in the ⊘ case.

Γ_{11}; Π_{11} ⊢ A; Δ_{11} Γ_{12}; Π_{12} ⊢ Σ_{12}, B, Σ′_{12}; Δ_{12}

Γ_{11}, Π_{11}, Γ_{12}; Π_{12} ⊢ Σ_{12}, A ⊘ B, Σ′_{12}; Δ_{11}, Δ_{12}

Γ_{2}, A; Π_{2}, B, Π′_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}; Π_{2}, A ⊘ B, Π′_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, Γ_{11}, Π_{11}, Γ_{12}; Π_{2}, Π_{12}, Π′_{2} ⊢ Σ_{12}, Σ_{2}, Σ′_{12}; Δ_{2}, Δ_{11}, Δ_{12}

⟹ Γ_{12}; Π_{12} ⊢ Σ_{12}, B, Σ′_{12}; Δ_{12}

Γ_{11}; Π_{11} ⊢ A; Δ_{11} Γ_{2}, A; Π_{2}, B, Π′_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, Γ_{11}, Π_{11}; Π_{2}, B, Π′_{2} ⊢ Σ_{2}; Δ_{2}, Δ_{11}
Γ_{2}, Γ_{11}, Π_{11}, Γ_{12}; Π_{2}, Π_{12}, Π′_{2} ⊢ Σ_{12}, Σ_{2}, Σ′_{12}; Δ_{2}, Δ_{11}, Δ_{12}

Note that this has eliminated the use of the ⊘ and introduced two cuts, (llcut) and (lccut). The planarity restrictions are equivalent in the (llcut) before and after the rewrite. There is an alternative possible rewrite, with the (llcut) on B above the (lccut) on A, and some instances of exchange to get the “classical” parts of the sequent in the right order; since one can easily permute cuts, this is essentially equivalent to what we have above.

• (Permuting (llcut) and ⊗): We illustrate the ⊗ case, where the cut formula is introduced in the premises.

Γ_{11}; Π_{11} ⊢ Σ_{11}, A; Δ_{11} Γ_{12}; Π_{12} ⊢ B, Σ_{12}; Δ_{12}

Γ_{11}, Γ_{12}; Π_{11}, Π_{12} ⊢ Σ_{11}, A ⊗ B, Σ_{12}; Δ_{11}, Δ_{12}

Γ_{2}; Π_{2}, A, B, Π′_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}; Π_{2}, A ⊗ B, Π′_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, Γ_{11}, Γ_{12}; Π_{2}, Π_{11}, Π_{12}, Π′_{2} ⊢ Σ_{11}, Σ_{2}, Σ_{12}; Δ_{2}, Δ_{11}, Δ_{12}

⟹ Γ_{12}; Π_{12} ⊢ B, Σ_{12}; Δ_{12}

Γ_{11}; Π_{11} ⊢ Σ_{11}, A; Δ_{11} Γ_{2}; Π_{2}, A, B, Π′_{2} ⊢ Σ_{2}; Δ_{2}
Γ_{2}, Γ_{11}; Π_{2}, Π_{11}, B, Π′_{2} ⊢ Σ_{11}, Σ_{2}; Δ_{2}, Δ_{11}
Γ_{2}, Γ_{11}, Γ_{12}; Π_{2}, Π_{11}, Π_{12}, Π′_{2} ⊢ Σ_{11}, Σ_{2}, Σ_{12}; Δ_{2}, Δ_{11}, Δ_{12}

Note that although the planarity conditions for these two derivations are not equivalent, the one for the first does imply the one for the second, so that if the first is a well-formed derivation, so is the second. We leave the variants involving the variant linear-linear cuts to the reader (in this and other cases). And so we conclude our selection from the proof of cut elimination.

Cut elimination induces a notion of equivalence of derivations in the usual manner; we would expect that this is reflected in our semantics given by bicontextual weakly distributive categories, in other words, that cut elimination is modelled soundly in any such category. This means that we have some rather large commutative diagrams to verify.

To make the statement of categorical cut elimination accessible, it may be thought desirable to give an explicit list of the commuting diagrams required of bicontextual weakly distributive categories. We have provided, instead, a recipe which does allow the reader to generate them all. Despite this, we do feel we are in a position to claim the following theorem. Theorem 4.2 Cut elimination is modelled soundly in any bicontextual weakly distributive category.

The proof of this is quite an intimidating exercise in diagram chasing—some cases involve several dozen cells in their decomposition. We believe this will become much simpler with the development of a suitable notion of proof nets for the context calculus. We plan to explore proof nets for the context calculus in a sequel, and that would be a more suitable place to present the details of a proof of this result.

That said, we have in fact checked the direct diagram-chase proof in detail. We shall illustrate the diagram-chase proof with one simple example. Permuting (lccut) and (⊘ thin) amounts to the commutativity of the outer paths of the following diagram; the inner cells prove its commutativity. We are starting with morphisms f: G_{1} ⊘ P_{1} ⟶ A ⦸ D and g: G_{2} ⊘ (G′_{2} ⊘ P_{2}) ⟶ W; g may be ignored as it is the last arrow composed in both sides.

[figure: (G_{2} ⊘ (A ⊘ G′_{2})) ⦸ D; (1 ⊘ e) ⦸ 1; (G_{2} ⊘ G′_{2}) ⦸ D; δ_{L}^{L}; δ_{L}^{L}; G_{2} ⊘ ((A ⊘ G′_{2}) ⦸ D); 1 ⊘ (e ⦸ 1); G_{2} ⊘ (G′_{2} ⦸ D); i; 1 ⊘ δ_{L}^{R}; 1 ⊘ i; G_{2} ⊘ ((A ⦸ D) ⊘ G′_{2}); 1 ⊘ e; G_{2} ⊘ G′_{2}; 1 ⊘ (f ⊘ 1); 1 ⊘ e; G_{2} ⊘ ((G_{1} ⊘ P_{1}) ⊘ G′_{2}); 1 ⊘ e; 1 ⊘ a; 1 ⊘ (1 ⊘ e); G_{2} ⊘ (G_{1} ⊘ (P_{1} ⊘ G′_{2})); 1 ⊘ e; G_{2} ⊘ (P_{1} ⊘ G′_{2})]

The key cell in this diagram is the costrength of e:

[figure: (A ⊘ G′_{2}) ⦸ D; e ⦸ 1; G′_{2} ⦸ D; δ_{L}^{R}; i; (A ⦸ D) ⊘ G′_{2}; e; G′_{2}]

□

References

[Be94] Benton P.N. “A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Preliminary Report)”, Technical Report 352, University of Cambridge, Computer Laboratory, 1994.

[BBPH] Benton P.N., G. Bierman, V. de Paiva, M. Hyland “Term assignment for intuitionistic linear logic”, M. Bezem and J. F. Groote, eds, Proceedings of the International Conference on Typed Lambda Calculi and Applications, 1992, Springer Lecture Notes in Computer Science 664, 75–90.

[B95] Bierman, G.M. “What is a categorical model of intuitionistic linear logic?”, in M. Dezani, ed, Proceedings of Conference on Typed lambda calculus and Applications, 1995, Springer-Verlag. (Also: Technical Report 333, University of Cambridge, 1994.)

[B92] Blute, R.F. “Linear Logic, Coherence and Dinaturality”, Theoretical Computer Science 115 (1992) 3–42.

[BCS92] Blute, R.F., J.R.B. Cockett, and R.A.G. Seely “ ! and ? : Storage as tensorial strength”, Mathematical Structures in Computer Science 6 (1996) 313–351.

[BCST] Blute R.F., J.R.B. Cockett, R.A.G. Seely, and T.H. Trimble “Natural deduction and coherence for weakly distributive categories”, to appear in Journal of Pure and Applied Algebra, (Preprint, McGill University, 1992, revised 1994).

[Bo94] Borceux, F. Handbook of Categorical Algebra, Cambridge University Press, 1994.

[C86] Cartmell, J. “Generalized Algebraic Theories and Contextual Categories”, Annals of Pure and Applied Logic, 32 (1986), 209–243

[C91] Cockett J.R.B., D.L. Spencer “Strong categorical datatypes I”, in R.A.G. Seely, ed., Category Theory 1991, Montreal, CMS Conference Proceedings, 13 (1991), 141–169.

[CS91] Cockett, J.R.B. and R.A.G. Seely “Weakly distributive categories”, in M.P. Fourman, P.T. Johnstone, A.M. Pitts, eds., Applications of Categories to Computer Science, London Mathematical Society Lecture Note Series 177 (1992) 45–65. (Expanded version to appear in Journal of Pure and Applied Algebra.)

[CS96] Cockett, J.R.B. and R.A.G. Seely “Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories”, preprint, McGill University, 1996.

[G93] Girard, J.-Y. “On the unity of logic”, Annals of Pure and Applied Logic 59 (1993) 201–217.

[LS86] Lambek, J. and P.J. Scott Introduction to Higher-Order Categorical Logic. Cambridge studies in advanced mathematics 7, Cambridge University Press, 1986.

[M93] Milner, R. “Action calculi, or concrete action structures”, Mathematical Foundations of Computer Science, Springer Lecture Notes in Computer Science 711 (1993), 105–121.

[M89] Moggi, E. “Computational lambda calculus and monads”, Proceedings IEEE Symposium on Logic in Computer Science, (Fourth Annual, 1989).

[PR89] Paré, R. and L. Román “Monoidal categories with natural numbers object”, Studia Logica XLVIII (1989) 361–376.

[P96] Pavlović, D. “Categorical logic of names and abstraction in action calculi”, to appear in Mathematical Structures in Computer Science.

[PR96] Power, A.J. and E.P. Robinson “Premonoidal categories and notions of computation”, Preprint, 1996.

[S89] Seely, R.A.G. “Linear logic, ∗-autonomous categories and cofree coalgebras”, in J. Gray and A. Scedrov (eds.), Categories in Computer Science and Logic, Contemporary Mathematics 92 (Am. Math. Soc. 1989).