Keywords

1 Introduction

Skew monoidal categories are a weakening of Mac Lane’s monoidal categories in which the structural laws \(\lambda \), \(\rho \) and \(\alpha \) are not required to be invertible, they are merely natural transformations with a specific orientation. They were introduced by Szlachányi in his study of bialgebroids [27] and have subsequently been investigated by many (mostly Australian) category theorists [3, 5, 7, 19, 20]. In programming language semantics, skew monoidal categories prominently appear as a categorical framework for the study of relative monads [1]: similarly to monads on a category \(\mathbb {C}\), which are characterized as monoids in the monoidal category of endofunctors on \(\mathbb {C}\), relative monads on a functor \(J : \mathbb {J}\rightarrow \mathbb {C}\) are monoids in the skew monoidal category of functors between \(\mathbb {J}\) and \(\mathbb {C}\).

Skew monoidal categories have received notable attention in recent years in connection to their coherence problem. For (normal, non-skew) monoidal categories, Mac Lane [22] showed that each homset in the free monoidal category generated by a set of objects contains at most one map, and exactly one when the domain and codomain have the same frontier of generating objects, i.e. generating objects appear in the same order and with same multiplicity. The same is not true in the free skew monoidal category: there exist pairs of objects with the same frontier but with either no maps or multiple maps between them. This peculiarity spawned the search for concrete presentations of the free skew monoidal category, or searching for sufficient conditions for the existence of a unique map between two objects. Taking a rewriting approach, Uustalu [28] showed that there is at most one map between an object and an object in a certain normal form, and exactly one map between an object and that object’s normal form. Lack and Street [20], and successively also Bourke and Lack [4], addressed the problem of determining equality of maps by proving that there is a faithful, structure-preserving functor from the free skew monoidal category on one generating object to the category \(\varDelta _{\bot }\) of finite non-empty ordinals and first-element-and-order-preserving functions.

Uustalu et al. [29] solved the coherence problem for skew monoidal categories by constructing a focused (in the sense of Andreoli [2]) sequent calculus in which sequent derivations are in one-to-one correspondence with maps in the free skew monoidal category. From the focused calculus, one can extract algorithms solving the following problems in the free skew monoidal category: (1) deciding equality of parallel maps; (2) enumerating all maps in a certain homset, which is a meaningful problem only in the skew case in which not all parallel maps are equal. This proof-theoretic approach to coherence is inspired by the pioneering work of Lambek on deductive systems for residuated categories [21], which many authors have successfully applied in subsequent years to other categories with structure, such as Szabo [26], Mints [24], and Dosen and Petrić [12]. Recently, Zeilberger revived this line of work in his study of the Tamari order [33].

In this paper, we continue following Lambek’s footsteps and study the proof theory of symmetric skew monoidal categories, again for the purpose of coherence. An appropriate notion of symmetry (and, more generally, braiding) for skew monoidal categories have recently been introduced by Bourke and Lack [6] (which we recollect in Sect. 2): the original symmetry of Mac Lane [22], typed \(B \otimes C \rightarrow C \otimes B\), is replaced by a symmetry typed \((A \otimes B) \otimes C \rightarrow (A \otimes C) \otimes B\), exclusively allowing the swapping of the second and third objects B and C, leaving the first object A in its place. Mac Lane’s coherence for symmetric (normal, non-skew) monoidal categories states that two parallel maps in the free symmetric monoidal category are equal if and only if they have the same underlying permutation of generating objects. Analogously to the skew monoidal case, this is not true in the free symmetric skew monoidal category, and this peculiarity leads again to a more sophisticated solution to the coherence problem.

The central contribution of this paper resides in the introduction of three equivalent presentations of the free symmetric skew monoidal category on a set of generators: a Hilbert-style categorical calculus (Sect. 3), a cut-free sequent calculus (Sect. 4) and a focused subsystem of the latter (Sect. 5), implementing a sound and complete backward proof search strategy attempting to build a derivation in the sequent calculus. Similarly to the skew monoidal case of Uustalu et al. [29], the sequent calculus has peculiar sequents of the form \(S \mid \varGamma \vdash C\), where the antecedent is split into an optional formula S, called the stoup, and a list of formulae \(\varGamma \), called the context. The symmetry \((A \otimes B) \otimes C \rightarrow (A \otimes C) \otimes B\) is modelled via a restrained exchange rule, which allows the permutation of formulae in the context but leaves the formula in the stoup unchanged. Our sequent calculus can be seen as a restricted variant of the \(\mathsf {I},\otimes \) fragment of intuitionistic linear logic [16]. Focusing defines a normalization procedure for maps in the free symmetric skew monoidal category, as such solving the coherence problem for symmetric skew monoidal categories. Following Uustalu et al. [30], we also discuss an extension of the focused sequent calculus, defining a concrete presentation of the free normal symmetric monoidal category and recover the original Mac Lane coherence theorem for symmetric monoidal categories (Sect. 6).

The material presented in Sects. 3, 4 and 5 have been formalized in the Agda proof assistant, the code is available at https://github.com/niccoloveltri/coh-symmskewmon.

2 Braided/Symmetric Skew Monoidal Categories

A category \(\mathbb {C}\) is (left-)skew monoidal [27] if it is equipped with a distinguished object \(\mathsf {I}\), a functor \(\otimes : \mathbb {C}\times \mathbb {C}\rightarrow \mathbb {C}\) and three natural transformations

$$ \lambda _{A} : \mathsf {I}\otimes A \rightarrow A \qquad \rho _{A} : A \rightarrow A \otimes \mathsf {I}\qquad \alpha _{A,B,C} : (A \otimes B) \otimes C \rightarrow A \otimes (B \otimes C) $$

satisfying the equations

figure a
figure b
figure c

The latter equations are directed versions of the original Mac Lane axioms [22] for monoidal categories. Kelly [18] observed that, in the monoidal case, equations (m1), (m3), and (m4) follow from (m2) and (m5). In the skew situation, this is not the case.

A skew monoidal category is braided [6] if it is additionally equipped with a natural isomorphism

$$ s_{A,B,C} : (A \otimes B) \otimes C \rightarrow (A \otimes C) \otimes B $$

satisfying the equations

figure d
figure e
figure f
figure g

The braiding s is a symmetry if it is its own inverse, i.e. \(s^{-1} = s\). The structural law s is a restricted version of the usual braiding of Joyal and Street [17] in normal braided monoidal categories typed \(B \otimes C \rightarrow C \otimes B\). Now the leftmost object (A in the type of s above) is not allowed to be swapped with the other objects B and C. This implies the existence of a map between any two objects of the form \((\ldots ((A \otimes B_1) \otimes B_2) \ldots ) \otimes B_n\) and \((\ldots ((A \otimes B_{i_1}) \otimes B_{i_2}) \ldots ) \otimes B_{i_n}\), where \(i_1,\ldots ,i_n\) is a permutation of \(1,\ldots ,n\), and the object A is required to stay in its place. At first sight, equations (b1)-(b4) look very different from the usual equations of normal braided monoidal categories, but they are reminiscent of an alternative presentation by Davydov and Runkel via b-structures [10]. They also appear, with minor variations, as the coherence conditions for operadic trees of Curien et al. [9]. Bourke and Lack [6] showed that, when the left unitor \(\lambda \) is invertible, a braiding typed \(B \otimes C \rightarrow C \otimes B\) is derivable:

figure h

and moreover the braided skew monoidal structure is normal braided monoidal. In particular, \(\rho \) and \(\alpha \) are also invertible.

Example 1

The category \(\mathbf {Ptd}\) of pointed sets and point-preserving maps has the following symmetric skew monoidal structure. The unit is \(\mathsf {I}= (1,\star )\), where 1 is the singleton set with unique element \(\star \). The tensor of two pointed sets (A, a) and (B, b) is \((A,a) \otimes (B,b) = (A + B,\mathsf {inl}(a))\), where \(A+B\) is the disjoint union of A and B, and \(\mathsf {inl}\) is the injection of A into \(A + B\). The structural laws \(\lambda \) and \(\rho \) are not invertible, while \(\alpha \) is an isomorphism. The natural isomorphism \(s : ((A+B) + C,\mathsf {inl}(\mathsf {inl}(a))) \rightarrow ((A+C) + B,\mathsf {inl}(\mathsf {inl}(a)))\) is defined using the symmetry and associativity of disjoint union.

This example is an instance of a more general phenomenon discussed by Bourke and Lack [6]: given a braided (resp. symmetric) monoidal category \(\mathbb {C}\) and a monoid M in \(\mathbb {C}\), then the category of left M-modules is braided (resp. symmetric) skew monoidal. The example above arises by taking \(\mathbb {C}\) as the category of sets and functions with the symmetric monoidal structure given by disjoint union, and the monoid M as the singleton set 1. The category of left 1-modules is isomorphic to \(\mathbf {Ptd}\).

Example 2

Given a braided (skew) monoidal category \((\mathbb {C}, \mathsf {I}, \otimes )\) and a comonad \((D,\varepsilon ,\delta )\) on \(\mathbb {C}\). Suppose D is lax braided monoidal, i.e., comes with a map \(\mathsf {e}: \mathsf {I}\rightarrow D\, \mathsf {I}\) and a natural transformation \(\mathsf {m}: D\, A \otimes D\, B \rightarrow D\, (A \otimes B)\) agreeing suitably with \(\lambda \), \(\rho \), \(\alpha \), s, \(\varepsilon \), \(\delta \). The category \(\mathbb {C}\) has another braided skew monoidal structure \((\mathsf {I}, \otimes ^D)\) where \(A \otimes ^D B = A \otimes D\, B\). The unitors, associator and braiding are:

figure i

If the braiding s of \(\mathbb {C}\) is a symmetry and D is lax symmetric monoidal, then \(s^D\) is a symmetry as well.

3 The Free Symmetric Skew Monoidal Category

The free symmetric skew monoidal category \(\mathbf {Fssk}(\mathsf {At})\) over a set \(\mathsf {At}\) (of atoms) can be defined as a Hilbert-style deductive system, which we call the categorical calculus. Objects of \(\mathbf {Fssk}(\mathsf {At})\) are formulae inductively generated as follows: either an atom \(X \in \mathsf {At}\); \(\mathsf {I}\); or \(A \otimes B\) where A, B are formulae. We write \(\mathsf {Fma}\) for the set of formulae. Maps between two formulae A and C are derivations of (singleton-antecedent, singleton-succedent) sequents \(A \Longrightarrow C\), constructed using the following inference rules:

(1)

and identified up to the congruence \(\doteq \) induced by the equations in Fig. 1.

The categorical calculus defines the free symmetric skew monoidal category on \(\mathsf {At}\) in a direct way. Given another symmetric skew monoidal category \(\mathbb {C}\) with function \(G : \mathsf {At}\rightarrow \mathbb {C}\), we can easily define mappings \(\overline{G}_0 : \mathsf {Fma}\rightarrow \mathbb {C}_0\) and \(\overline{G}_1 : (A \Longrightarrow C) \rightarrow \mathbb {C}(\overline{G}_0(A),\overline{G}_0(C))\) by induction. These specify a strict symmetric monoidal functor, in fact the only existing one satisfying \(\overline{G}_0(X) = G(X)\).

Define the frontier \(\delta (A)\) of a formula A as the ordered list of atoms contained in A. Given an ordered list l with length n and an element \(\sigma \) of the symmetric group on n elements, i.e. a permutation of n elements, we write \(\sigma \cdot l\) for the action of \(\sigma \) on l.

Mac Lane [22] proved a coherence theorem for (normal, non-skew) symmetric monoidal categories, which can be phrased as follows: given two formulae A and C in the free symmetric monoidal category, there exists a map typed \(A \Longrightarrow C\) iff there exists a permutation \(\sigma \) such that \(\delta (C) = \sigma \cdot \delta (A)\) (which is to say that \(\delta (A)\) and \(\delta (C)\) are equal as multisets) and, if this is the case, two parallel maps in \(A \Longrightarrow C\) are equal iff they have the same underlying permutation \(\sigma \).

For the free symmetric skew monoidal category, this is not the case. First, there exist pairs of formulae with the exact same frontier but with no maps between them: there are no maps typed \(X \Longrightarrow \mathsf {I}\otimes X\), no maps typed \(X \otimes \mathsf {I}\Longrightarrow X\) and no maps typed \(X \otimes (Y \otimes Z) \Longrightarrow (X \otimes Y) \otimes Z\). There are also no maps typed \(X \otimes Y \Longrightarrow Y \otimes X\). Moreover, there are multiple maps between formulae with the exact same frontier: there are two maps and two maps . Bourke and Lack [6] showed that there are two maps . Postcomposing the latter two maps with s, we obtain two distinct maps typed \(((X \otimes \mathsf {I}) \otimes Y) \otimes Z \Longrightarrow (X \otimes Z) \otimes Y\) which have underlying permutation of frontiers \(\sigma = (132)\).

Fig. 1.
figure 1

Equivalence of derivations in the categorical calculus

Full size image

4 Symmetric Skew Monoidal Sequent Calculus

The free symmetric skew monoidal category \(\mathbf {Fssk}(\mathsf {At})\) admits an equivalent presentation as a cut-free sequent calculus. Formulae are again elements of \(\mathsf {Fma}\). Similarly to the non-symmetric case worked out in a previous paper [29], sequents are triples of the form \(S \mid \varGamma \vdash C\). The antecedent of the sequent is split in two parts: S is an optional formula called the stoup, which can either be empty (which we denote \({-}\)) or a single formula, and \(\varGamma \) is an ordered list of formulae, that we call the context. The succedent C is a single formula. Derivations of sequents \(S \mid \varGamma \vdash C\) are generated by the following inference rules:

(2)

(\(\mathsf {pass}\) for ‘passivate’, \(\mathsf {ex}\) for ‘exchange’, \(\mathsf {L}\), \(\mathsf {R}\) for introduction on the left (in the stoup) resp. right) and identified up to the congruence \(\circeq \) induced by the equations in Fig. 2.

Fig. 2.
figure 2

Equivalence of derivations in the sequent calculus

Full size image

The rules \(\mathsf {I}\mathsf {L}\), \(\otimes \mathsf {L}\) and \(\mathsf {ex}\) are invertible up to \(\circeq \), but the passivation rule \(\mathsf {pass}\) is not. General forms of exchange, swapping a formula with a list of formulae, are admissible by induction on the list of formulae \(\varXi \):

(3)

Two forms of cut are admissible, satisfying a large number of \(\circeq \)-equations (see [29, Figures 5 and 6] for the list of such equations not involving the exchange rule \(\mathsf {ex}\)).

(4)

The inference rules in (2) are reminiscent of the rules of the \(\mathsf {I},\otimes \) fragment of intuitionistic linear logic, but there are some crucial differences/restrictions:

  1. 1.

    The left rules \(\mathsf {I}\mathsf {L}\) and \(\otimes \mathsf {L}\) act only on the formula in the stoup. In particular, there are no rules for decomposing a unit \(\mathsf {I}\) or a tensor \(A\otimes B\) in the context. This allows the derivability of sequents corresponding to the right unitor \(\rho : A \Longrightarrow A \otimes \mathsf {I}\) and the associator \(\alpha : (A \otimes B) \otimes C \Longrightarrow A \otimes (B \otimes C)\), but not their inverses.

    figure j
  2. 2.

    There is a distinction between antecedents of the form \(A \mid \varGamma \), where the formula A is in the stoup, and antecedents of the form \({-}\mid A,\varGamma \), where A is out of the stoup. This distinction is crucial in the right rule \(\otimes \mathsf {R}\), which always sends the formula in the stoup to the first premise (when the rule is read bottom-up). This allows the derivability of a sequent corresponding to the left unitor \(\lambda : \mathsf {I}\otimes A \Longrightarrow A\), but not its inverse, since the passivation rule \(\mathsf {pass}\) is not invertible.

    figure k
  3. 3.

    The exchange rule \(\mathsf {ex}_{A,B}\) permits the swap of two adjacent formulae A and B in the context, but there is no way to generally swap a formula in the stoup with a formula in the context. This allows the derivability of a sequent corresponding to the symmetry \(s : (A \otimes B) \otimes C \Longrightarrow (A \otimes C) \otimes B\) involving three formulae, but not of a symmetry involving two formulae typed \(B \otimes C \Longrightarrow C \otimes B\).

    figure l

The sequent calculus rules in (2) accurately match the categorical calculus rules in (1), and the \(\circeq \)-equations in Fig. 2 match the \(\doteq \)-equations in Fig. 1, in very a precise sense. There exists an effective procedure \(\mathsf {sound}: (S \mid \varGamma \vdash C) \rightarrow (\llbracket S | \varGamma \rrbracket \Longrightarrow C)\) turning a sequent calculus derivation into a categorical calculus derivation, where the interpretation of an antecedent as a formula \(\llbracket S | \varGamma \rrbracket \) is defined as \(\llbracket S | \varGamma \rrbracket = \llbracket S \langle \langle \, \, \langle \langle \varGamma \rrbracket \) with

$$ \llbracket {-} \langle \langle \, = \mathsf {I}\qquad \llbracket A \langle \langle \, = A \qquad \qquad A\, \langle \langle ~ \rrbracket = A \qquad A\, \langle \langle B,\varGamma \rrbracket = (A \otimes B)\, \langle \langle \varGamma \rrbracket $$

which means that \(A\, \langle \langle A_1, A_2 \ldots , A_n \rrbracket = (\ldots (A \otimes A_1) \otimes A_2) \ldots ) \otimes A_n\). The function \(\mathsf {sound}\) is well-defined, in the sense that it sends \(\circeq \)-related derivations to \(\doteq \)-related derivations. There exists also an effective procedure \(\mathsf {cmplt}: (\llbracket S | \varGamma \rrbracket \Longrightarrow C) \rightarrow (S \mid \varGamma \vdash C)\) which is the inverse of \(\mathsf {sound}\) up to the equivalences \(\doteq \) and \(\circeq \), i.e. \(\mathsf {sound}(\mathsf {cmplt}(f))\doteq f\), for all \(f : \llbracket S | \varGamma \rrbracket \Longrightarrow C\), and \(\mathsf {cmplt}(\mathsf {sound}(g)) \circeq g\), for all \(g : S \mid \varGamma \vdash C\). Composition \(f \circ g\) in the categorical calculus is intepreted by \(\mathsf {cmplt}\) as \(\mathsf {scut}(\mathsf {cmplt}(g),\mathsf {cmplt}(f))\). The function \(\mathsf {cmplt}\) is also well-defined, i.e. it sends \(\doteq \)-related derivations to \(\circeq \)-related derivations.

Theorem 1

The set of derivations of the sequent \(S \mid \varGamma \vdash C\), quotiented by the equivalence relation \(\circeq \), is isomorphic to the set of derivations of the sequent \(\llbracket S | \varGamma \rrbracket \Longrightarrow C\), quotiented by the equivalence relation \(\doteq \).

This shows that the cut-free sequent calculus is an equivalent presentation of the free symmetric skew monoidal category \(\mathbf {Fssk}(\mathsf {At})\).

5 A Focused Subsystem for the Symmetric Skew Case

The free symmetric skew monoidal category admits a more concrete presentation as a focused sequent calculus. Derivations in this calculus correspond to canonical representatives of equivalence classes of the relation \(\circeq \). They are generated by the following inference rules:

(5)

(T is always an optional atom, i.e. either empty or an atomic formula.) As in Andreoli’s original formulation for linear logic [2], the focused calculus defines a goal-directed proof search strategy which attempts to build a derivation of a sequent in the cut-free sequent calculus of Sect. 4, starting from the root:

  • We start in phase \(\mathsf {C}\) (for ‘context’) by permuting the formulae in the context. This is performed step-by-step using the rule \(\mathsf {exs}\), moving one formula at the time, in a way reminiscent of the insertion-sort algorithm. In this phase, contexts are split in two parts , where \(\varGamma \) consists of formulae that have already been moved by \(\mathsf {exs}\) and the formulae in \(\varOmega \) are yet to be moved. Once all the formulae have been moved, so the antecedent is of the form , we switch to phase \(\mathsf {L}\) using the rule \(\mathsf {sw}_{\mathsf {LC}}\).

  • In phase \(\mathsf {L}\) (for ‘left’), the formula in the stoup is eagerly decomposed using the invertible left rules \(\mathsf {I}\mathsf {L}\) and \(\otimes \mathsf {L}\). The premise of the \(\otimes \mathsf {L}\) rule is a derivation of a sequent in phase \(\mathsf {C}\), which gives the chance to further move the formula B in a different position of the context. If the stoup is empty we have the possibility of applying the \(\mathsf {pass}\) rule, i.e. moving the leftmost formula A in the context to the stoup, and continue the decomposition of A. When the formula in the stoup is fully decomposed, i.e. either the stoup is empty or it contains an atomic formula, we switch to phase \(\mathsf {R}\) using the rule \(\mathsf {sw}_{\mathsf {RL}}\). Notice that, when the stoup is empty, we are not obliged to use the \(\mathsf {pass}\) rule, so we have a choice between applying \(\mathsf {pass}\) and \(\mathsf {sw}_{\mathsf {RL}}\).

  • In phase \(\mathsf {R}\) (for ‘right’), we focus on the succedent formula. Depending on its shape, only one among the rules \(\mathsf {ax}\), \(\mathsf {I}\mathsf {R}\), \(\otimes \mathsf {R}\) can be applied. The second premise of the \(\otimes \mathsf {R}\) rule is a derivation of a sequent in phase \(\mathsf {L}\), which gives the chance of applying the \(\mathsf {pass}\) rule and subsequently the invertible left rules \(\mathsf {I}\mathsf {L}\) and \(\otimes \mathsf {L}\). Different ways of splitting the context in an application of the rule \(\otimes \mathsf {R}\) can lead to different successful derivations, which is another source of nondeterminism.

By dropping the phase annotations (also turning into a comma), we can define three functions \(\mathsf {emb}_{\mathsf {C}}\), \(\mathsf {emb}_{\mathsf {L}}\) and \(\mathsf {emb}_{\mathsf {R}}\) embedding focused sequent calculus derivations in the unfocused sequent calculus. The function interprets the focused rule \(\mathsf {exs}_{A,\varGamma }\) in (5) as the admissible unfocused rule \(\mathsf {exs}_{A,\varGamma }\) in (3). We can also define a normalization function , which maps \(\circeq \)-related derivations to equal focused derivations. For the definition of \(\mathsf {focus}\), all the unfocused rules in (2) are proved admissible in phase C. The functions \(\mathsf {focus}\) and \(\mathsf {emb}_\mathsf {C}\) establish a bijection between the sequent calculus and its focused subsystem: \(\mathsf {emb}_{\mathsf {C}}\; (\mathsf {focus}\;f) \circeq f\) and \(\mathsf {focus}\;(\mathsf {emb}_{\mathsf {C}}\;g) = g\), for all \(f : S \mid \varGamma \vdash C\) and .

Theorem 2

The following are isomorphic:

  1. (i)

    the set of derivations of the sequent ;

  2. (ii)

    the set of derivations of the sequent \(S \mid \varOmega \vdash C\), quotiented by the equivalence relation \(\circeq \);

  3. (iii)

    the set of derivations of the sequent \(\llbracket S | \varGamma \rrbracket \Longrightarrow C\), quotiented by the equivalence relation \(\doteq \).

The focused sequent calculus is peculiar in that it gives the ability of having a “change of mind” regarding the position to which a formula is moved during phase \(\mathsf {C}\). To explain this phenomenon, consider for example the two derivations of , which in the categorical calculus correspond to distinct maps :

(6)

On the left, the formulae in the context are never swapped. On the right, first X is swapped with \(\mathsf {I}\otimes Y\) (the \(\mathsf {exs}\) rule), then Y is swapped with X (the \(\mathsf {exs}\) rule). The second exchange is necessary for completing the derivation. This means that we are allowed to move the atom X past the atom Y (initially inside the composite formula \(\mathsf {I}\otimes Y\)) and subsequently change our mind and swap the positions of X and Y again. The construction of two such distinct focused derivations with the same underlying permutation of atoms (in this case the identity permutation fixing X and Y) is possible since the atom Y is wrapped in the composite formula \(\mathsf {I}\otimes Y\), whose leftmost formula \(\mathsf {I}\) is closed, i.e. free of atoms: in the right derivation in (6), when \(\mathsf {I}\otimes Y\) is moved to the stoup, after an application of the rule \(\otimes \mathsf {L}\) we have the possibility of swapping Y and X again and subsequently the unit \(\mathsf {I}\) in the stoup is removed with an application of \(\mathsf {I}\mathsf {L}\). This “change of mind”, in which we apply the rule \(\mathsf {exs}\) on the same atom multiple times, is only possible in the skew case, the same is not doable in the focused sequent calculus of symmetric monoidal categories (see the next section).

The separation of the context in two parts in phase \(\mathsf {C}\) takes inspiration from Chaudhuri and Pfenning’s focused sequent calculus for linear logic [8], and it also appears in the design of focused sequent calculi for right-normal and associative-normal skew monoidal categories [30].

6 Recovering Coherence for the Non-Skew Case

The focused sequent calculus in (5) can be expanded and modified in order to obtain a concrete presentation of the free symmetric monoidal category and recover Mac Lane’s coherence theorem [22]. This is in analogy with Uustalu et al.’s recovery of the coherence theorem for monoidal categories starting from a focused sequent calculus for skew monoidal categories [30].

(7)

(Condition \(S \not = X\) in rule \(\mathsf {sw}_{\mathsf {LC}}\) requires the stoup S to not be an atomic formula. Condition \(T = {-}\rightarrow \varGamma = ()\) in rule \(\mathsf {sw}_{\mathsf {RL}}\) requires the context \(\varGamma \) to be empty whenever the stoup T is empty.)

The differences with the focused sequent calculus in (5) are:

  • In phase \(\mathsf {C}\), the new rules \(\mathsf {IC}\) and \(\otimes \mathsf {C}\) allow the decomposition of units and tensors in the context, and correspond to adding inverses for \(\rho \) and \(\alpha \) in the categorical calculus (1) (see Sects. 3.2 and 3.3 of [30] for a discussion on this correspondence). The modified \(\mathsf {exs}\) rule now acts only on atomic formulae. This implies that each sequent appearing in the derivation of a valid sequent has the context \(\varGamma \) consisting only of atomic formulae. Once all atoms have been moved using \(\mathsf {exs}\) and the antecedent is of the form , we check whether the formula in the stoup is an atom: if it is, we move it in the context using the new rule \(\mathsf {exs}^{\mathsf {S}}\), otherwise we switch to phase \(\mathsf {L}\) using the rule \(\mathsf {sw}_{\mathsf {LC}}\) as before.

  • Rules \(\mathsf {I}\mathsf {L}\), \(\otimes \mathsf {L}\) and \(\mathsf {pass}\) in phase \(\mathsf {L}\) are unchanged, but the condition in \(\mathsf {sw}_{\mathsf {RL}}\) for switching from phase \(\mathsf {L}\) to phase \(\mathsf {R}\) is more stringent: if the stoup is empty, we are allowed to switch phase only when the context is empty as well. This restriction forces all formulae in the context to be reduced to atoms using the rules \(\mathsf {IC}\), \(\otimes \mathsf {C}\), \(\mathsf {I}\mathsf {L}\) and \(\otimes \mathsf {L}\). In particular, in a successful derivation of a sequent , it is possible to switch to phase \(\mathsf {R}\) only if the antecedent is completely empty or all the formulae in the antecedents are atoms and the stoup is non-empty.

  • Phase \(\mathsf {R}\) contains a new rule \(\otimes \mathsf {R}_2\), which allows to send the atom in the stoup to the second premise, provided that all of the context is also sent to the second premise (so the antecedent of the first premise is left completely empty). The rule \(\otimes \mathsf {R}_2\), together with the restriction in \(\mathsf {sw}_{\mathsf {RL}}\) discussed above, correspond to adding an inverse for \(\lambda \) in the categorical calculus (1) (as explained in Sect. 3.1 of [30]).

The “change of mind” of the focused sequent calculus for symmetric skew monoidal categories, exemplified in the derivation on the right in (6), where the rule \(\mathsf {exs}\) can act multiple times on an atomic formula in the context, disappears in the focused sequent calculus for symmetric monoidal categories. Using rules in (7), the non-determinism exposed in (6) vanishes, and there is a unique derivation of the sequent :

figure o

More precisely, it is possible to prove that, in each derivation of a sequent in the focused sequent calculus (7), every atomic formula in \(S \mid \varOmega \) is moved exactly once in a (possibly) different position past the dotted line with an application of the rule \(\mathsf {exs}\) or the rule \(\mathsf {exs}^{\mathsf {S}}\). This shows that each successful derivation of a sequent is in one-to-one correspondence with a permutation of the frontier of A, which is a proof-theoretic formulation of Mac Lane’s coherence theorem for symmetric monoidal categories.

It is possible to find appropriate extensions of the categorical calculus of Sect. 3 (now defining the free symmetric monoidal category on \(\mathsf {At}\) in a direct way) and the cut-free sequent calculus of Sect. 4, and prove a theorem analogue to Theorem 2, stating that the focused sequent calculus (7) is equivalent to these extended calculi. As such, the focused sequent calculus (7) is a concrete presentation of the free symmetric monoidal category on \(\mathsf {At}\).

7 Conclusions and Future Work

We constructed three equivalent proof systems describing the free symmetric skew monoidal category \(\mathbf {Fssk}(\mathsf {At})\) on a set \(\mathsf {At}\): a Hilbert-style categorical calculus, a cut-free sequent calculus, and a subsystem of focused derivations of the latter. The focused sequent calculus solves the coherence problem for symmetric skew monoidal categories. It provides a decider for equality of maps in \(\mathbf {Fssk}(\mathsf {At})\): two parallel maps \(f, g: A \Longrightarrow C\) are \(\doteq \)-related iff \(\mathsf {focus}(\mathsf {cmplt}(f)) = \mathsf {focus}(\mathsf {cmplt}(g))\), and equality of focused derivations is decidable. It also gives a procedure for enumerating all maps in the homset \(A \Longrightarrow C\) up to the congruence \(\doteq \): simply count the number of focused derivations of the sequent . We showed how to extend the focused sequent calculus in order to obtain a calculus of normal forms for symmetric monoidal categories and retrieve Mac Lane’s coherence theorem using techniques from structural proof theory.

The story narrated in Sects. 3 and 4 applies with minor modifications to the more general case of braided skew monoidal categories, which we also formalized in Agda. The free braided skew monoidal category on a set of atoms has the same objects of \(\mathbf {Fssk}(\mathsf {At})\), but the grammar of derivations (1) is augmented with a new rule \(s^{-1}\) inverse (up to \(\doteq \)) of s. A sequent calculus for braided skew monoidal categories is obtained by including in the proof system (2) a new rule \(\mathsf {ex}^{-1}_{A,B}\) inverse (up to \(\circeq \)) of \(\mathsf {ex}_{A,B}\). As in the symmetric case, one can define effective procedures \(\mathsf {cmplt}\) and \(\mathsf {sound}\) translating between categorical calculus and sequent calculus, preserving the congruences \(\doteq \) and \(\circeq \), and exhibiting a bijection between the two deductive systems. However, the construction of a focused subsystem in the braided case does not seem obtainable as a simple generalization of the focused sequent calculus of Sect. 5. This complication is related to the representation of normal forms for braids in Artin braid groups, which is more convoluted that the representation of normal forms in symmetric groups [11, 14]. The rule \(\mathsf {exs}\) in (5) outlines an algorithm for constructing permutations of formulae in the context: starting from a context , repeated applications of \(\mathsf {exs}\) construct a context , where \(\varGamma \) is a permutation of \(\varOmega \), and all permutations can be represented in this way. A focused sequent calculus for the braided case will instead construct an action of the braid group on the formulae in the context, but such actions admit normal forms which are more arduous to formalize. After properly sorting out the proof theory of braided skew monoidal categories, it would be interesting to also understand the relationship between the resulting deductive systems and existing calculi for categories with braided structure [13, 15, 23].

In Sect. 6, we introduced a focused sequent calculus for normal symmetric monoidal categories and retrieve Mac Lane-style coherence. We plan to understand the relation between the latter proof system and Shulman’s practical type theory for symmetric monoidal categories [25]. We also plan to investigate the proof theory of partially normal symmetric skew monoidal categories in the style of [30], when one or both structural laws among \(\rho \) and \(\alpha \) are invertible (but not \(\lambda \), whose invertibility implies the invertibility of all structural laws [6]).

Finally, we want to study deductive systems for (symmetric) skew monoidal closed categories, which will include a linear implication \({\multimap }\) as in the proof systems for skew prounital closed categories [31]. The resulting calculi should allow the representation of interesting classes of concurrent computations, a skew variant of the concurrent logical framework of Watkins et al. [32].