Shufflings exhibit a particular property that motivates our next section: malleability. Any shuffling of $p₀$, $p₁$ and $p₂$ can be factored uniquely in two different forms: we can first shuffle $p₀$ and $p₁$ and then shuffle the result, $p₀ + p₁$, with $p₂$; or we can first shuffle $p₁$ and $p₂$, and then shuffle $p₀$ with the result, $p₁ + p₂$. For instance, any $1,2,3$-shuffling splits uniquely into a $2,3$-shuffling followed by a $1,5$-shuffling, but also uniquely into a $1,2$-shuffling followed by a $3,3$-shuffling.

Two factorizations of the previous shuffling.

This is a global property: any shuffling can be uniquely factored into smallest shufflings, in whichever arrangement we pick. Any morphism of the  $\mathbf{Shuf}$ can be factored into any possible shape, uniquely. We say that the multicategories that satisfy this property are “malleable multicategories”: shufflings form a .

§ MALLEABLE MULTICATEGORIES

A  is a  where each morphism can be morphed uniquely into any possible shape. This means that there exist unique factorizations of each morphism into each one of the possible shapes. Formally, we will define  to have an invertible composition, up to the morphisms of some underlying category.

The unary morphisms of a  form a category <cit.>.
In other words, given a  $𝕄$, the underlying category, $𝕄^u$, has the same objects as the multicategory, $𝕄_{obj}^u = 𝕄_{obj}$, and morphisms defined from the unary multimorphisms of the , $𝕄^u(X;Y) = 𝕄(X;Y)$. Composition and identities are exactly those of the .

The multimorphisms of a  determine profunctors over the underlying category of the .
The underlying category acts on the multimorphisms by composition,

\begin{align*}
& (≻) \colon 𝕄^u(X;X') × 𝕄(Γ₁,X',Γ₂;Y) → 𝕄(Γ₁,X,Γ₂;Y), \\
& (≺) \colon 𝕄(Γ;Y) × 𝕄^u(Y;Y') → 𝕄(Γ;Y').
\end{align*}

In any , composition of multimorphisms is dinatural with respect to the underlying category.
This follows from the associativity for ,

$$(f ≺ h) ⨾_{Xᵢ} g = (f ⨾_{X_i} h) ⨾_{X_i'} g = f ⨾_{X_i} (h ⨾_{X_i'} g) = f ⨾_{X_i} (h ≻ g).$$

As a consequence, composition is well-defined under dinaturality. We define dinatural composition to be composition lifted to the equivalence classes of the dinaturality equivalence relation, which are written as a coend,

$$\textstyle (⨾) \colon \left( ∫^{Y ∈ 𝕄} 𝕄(Γ;Y) × 𝕄(Γ₀,Y,Γ₁; Z)\right)  →  𝕄(Γ₀,Γ,Γ₁; Z).$$

A malleable multicategory is a  where dinatural composition is invertible.

with  between them form a category, $\mMult$. This is a wide subcategory of the category of .

If a multicategory is malleable, we can reconstruct it up to isomorphism from its binary and nullary maps.
When defining a , it is usually easier to provide its binary, unary and nullary maps, and deduce from those the rest of the structure. The situation is similar in monoidal categories: we do not need to provide the n-ary tensor in order to define a monoidal category, we only provide the binary and unary tensors.

This suggests that we will really work with a biased version of , one that privileges the binary and nullary tensors over the others. Biased malleable multicategories are better known as promonoidal categories.

§.§ Promonoidal Categories

In the same sense that multicategories provide an algebra for the composition of multiple pieces into one,
promonoidal categories provide an algebra for the coherent composition of multiple pieces into one. A category $ℂ$ contains sets of morphisms, $ℂ(X ; Y)$. In the same way, a promonoidal category $𝕍$ contains sets of joints, $𝕍(X_0 ◁ X_1; Y)$, morphisms, $𝕍(X; Y)$, and units, $𝕍(N; X)$, where $N$ is the virtual tensor unit.
Joints, $𝕍(X₀ ◁ X₁; Y)$, represent a way of joining objects of type $X₀$ and $X₁$ into an objects of type $Y$. Morphisms, $𝕍(X; Y)$, as in any category, are transformations of $X$ into $Y$. Units, $𝕍(N;Y)$, are the atomic pieces of type $Y$.

These compositions must now be coherent. For instance, imagine we want to join $X₀$, $X₁$ and $X₂$ into $Y$. Joining $X₀$ and $X₁$ into something $(•)$,  and then joining that something $(•)$ and $X₂$ into $Y$, should be doable in essentially the same ways as joining $X₁$ and $X₂$ into something $(•)$, and then joining $X₀$ and that something $(•)$ into $Y$. Formally, we are saying that,

∫^{U} 𝕍(X₀ ⊲ X₁ ; U) × 𝕍(U ⊲ X₂; Y)  ≅  ∫^{V} 𝕍(X₁ ⊲ X₂; V) × 𝕍(X₀ ⊲ V; Y),

and, in fact, we usually just write $𝕍(X₀ ⊲ X₁ ⊲ X₂; Y)$ for the set of such decompositions, even when it is only defined up to isomorphism.

are the 2-monoids of the monoidal bicategory of , which is equivalent to the following definition. A promonoidal category is a category $𝕍(• ; •)$ endowed with two

𝕍(• ⊲ • ; •) ፡ 𝕍 × 𝕍 → 𝕍, \mbox{ and } 𝕍(𝖭; •) ፡ 1 → 𝕍.

Equivalently, these are functors

𝕍(• ⊲ • ; •) ፡ 𝕍^{op} × 𝕍 × 𝕍 → \mathbf{Set}, \mbox{ and } 𝕍(𝖭; •) ፡ 𝕍^{op} → \mathbf{Set}.

Moreover,  must be endowed with the following natural isomorphisms,

\begin{align*}
𝕍(X₀ ⊲ X₁; •) ⋄ 𝕍(• ⊲ X₂ ; Y)    &≅  𝕍(X₁ ⊲ X₂; •) ⋄ 𝕍(X₀ ⊲ • ; Y);  \\
𝕍(𝖭; •) ⋄ 𝕍(• ⊲ X; Y)   &≅  𝕍(X; Y); \\
𝕍(𝖭; •) ⋄ 𝕍(X ⊲ •; Y)   &≅  𝕍(X; Y);
\end{align*}

called $α, λ, ρ$, respectively, and asked to satisfy the pentagon and triangle coherence equations,
$α ⨾ α = (α ⋄ \id) ⨾ α ⨾ (\id ⋄ α)$, and $(ρ ⋄ \id) = α ⨾ (λ ⋄ \id)$.

Let $𝕍$ and $𝕎$ be two . A promonoidal functor $F﹕ 𝕍 → 𝕎$ is a functor between the two categories together with natural transformations

\begin{align*}
& F_{⊲}﹕ 𝕍(X₀ ⊲ X₁; Y) → 𝕎(FX₀ ⊲ FX₁; FY),\ \mbox{ and }
& F_{𝖭} ﹕ 𝕍(𝖭; X) → 𝕎(𝖭; Y),
\end{align*}

that satisfy $λ ⨾ F_{map} = (F_{◁} × F_{N}) ⨾ λ$, $ρ ⨾ F_{map} = (F_{◁} × F_{N}) ⨾ ρ$, and $α ⨾ (F_{◁} × F_{◁}) ⨾ i = (F_{◁} × F_{◁}) ⨾ i ⨾ α$.

with  between them form a category, $\Prom$.

§.§ Promonoidal Categories are Malleable Multicategories

In this section, we show that the category of  is equivalent to that of . In this sense, the study of  is the study of .

Let $𝕍$ be a . There is a , $𝕍^m$, that has the same objects but multimorphisms defined by the elements of the . By induction, we define

\begin{align*}
& \textstyle{𝕍^m(X₀,X₁,Γ; Y) = ∫^V 𝕍(X₀ ⊲ X₁; V) × 𝕍^m(V,Γ;Y)}, \\
& 𝕍^m(X;Y) = 𝕍(X;Y), \\
& 𝕍^m(;Y) = 𝕍(𝖭; Y).
\end{align*}

In other words, the multimorphisms are elements of the left-biased tree reductions of the promonoidal category, seen as a 2-monoid.
Dinatural composition is then defined to be the unique map relating two tree expressions in a 2-monoid, which exists uniquely by coherence,

$$(\mathrm{coh}) \colon \left(\textstyle{∫^{X ∈ 𝕍}} 𝕍(Γ;X) × 𝕍^m(Γ₀,X,Γ₁; Y) \right) → 𝕍^m(Γ₀,Γ,Γ₁;X).$$

Coherence maps are isomorphisms, and so dinatural composition is invertible, making the multicategory coherent.
By coherence for pseudomonoids, composition must satisfy associativity and unitality.

The category of  and the category of  are equivalent with the functor  $(•)^m \colon \Prom → \mMult$ induced by the construction of the underlying  of a .
See a polycategorical analogue at <Ref>.

First, let us show that a , $F ፡ 𝕍 → 𝕎$, induces a multifunctor, $F^m ፡ 𝕍^m → 𝕎^m$ between the underlying multicategories.
On objects, we define it to be the same, $F^m_{obj} = F_{obj}$.
On multimorphisms, we define the binary, unary and nullary cases using the promonoidal transformations:

$$F^u_0 = F_N,\mbox{ with }F^u_1 = F_{map}\mbox{ and }F_2^u = F_{⊲}.$$

Then, we extend this definition to the n-ary case by induction, using $F^u_n = F_{⊲} × F_{n-1}^u$.
We now verify that this assignment is functorial: the only remarkable case is that of checking that the inductive case preserves composition.

\begin{align*}
(F ⨾ G)^u_n & \overset{(i)}{=} (F ⨾ G)_{⊲} × (F ⨾ G)^u_{n-1}
\overset{(ii)}{=} (F_{⊲} ⨾ G_{⊲}) × (F^u_{n-1} ⨾ G^u_{n-1}) \\
& \overset{(iii)}{=} (F_{⊲} × F^u_{n-1}) × (G_{⊲} × G^u_{n-1})
\overset{(iv)}{=} F^u_n ⨾ G^u_n.
\end{align*}

This equation holds because (i) of the inductive definition, (ii) the composition of promonoidal functors and the inductive hypothesis, (iii) the interchange law for functions, (iv) and the inductive definition.

We will now show that this is a fully faithful functor.
It is hopefully clear that it is faithful because $F^u = G^u$ directly implies $F_{obj} = G_{obj}$, $F_{⊲} = G_{⊲}$, $F_N = G_N$ and $F_{map} = G_{map}$. Let us show that it is also full. Let $G \colon 𝕍_u → 𝕎_u$ be a multifunctor between .
We will construct a  $G^\star$ such that $G^{\star u} = G$.
We start by defining that $G^\star_N = G_0$, that $G^\star_{map} = G_1$ and that $G^\star_{⊲} = G_2$. Now, we need to prove that $(G^{★ u})ₙ = Gₙ$. This is definitionally true for binary, unary and nullary multimorphisms; then, by induction,

$$Gₙ \overset{(i)}{=}
\decomp{} ⨾ (G₂ × Gₙ) \overset{(ii)}{=}
\decomp{} ⨾ (G₂^{\star u} × Gₙ^{\star u}) \overset{(iii)}{=}
G^{\star u}_n.$$

Here, we use (i) malleability, (ii) the induction hypothesis, and (iii) the definition of the underlying multifunctor. We have shown that we have a fully faithful functor.

Finally, we will show that $U ፡ \Prom → \mMult$ is essentially surjective. Given any malleable multicategory $𝕄$, we can define $M^{\flat}$ to be the  with the same objects and only binary, unary and nullary morphisms. We now note that there is an isomorphism, $𝕄 \cong 𝕄^{\flat u}$, that is the identity on objects. It is defined to use the invertible dinatural composition that exists by malleability,

\begin{align*}
𝕄_{\flat}^{u}(X₁,\dots,Xₙ;Y) & = \textstyle{∫^U} 𝕄(X₀,X₁;U) × 𝕄(U,X₂,\dots,Xₙ;Y) \\
& \cong 𝕄(X₁, \dots, Xₙ; Y).
\end{align*}

This makes the functor fully faithful and essentially surjective, defining an equivalence of categories.

§.§ Bibliography

What makes monoidal tensors universal? Products and coproducts have a universal property, but that is the exception and not the rule. Hermida's work <cit.> explains that tensors are universal because they represent a relevant multimap structure, a multicategory. For instance, the  of vector spaces with their tensor product represents functions linear in each variable: a linear function $A ⊗ B → C$ is the same as a multilinear function $A,B → C$.
Indeed, Lambek <cit.> first introduced  as the underlying structure that unified Gentzen's sequents and multilinear maps.

§ THE SPLICE-CONTOUR ADJUNCTION

§.§ Contour of a multicategory

This last section characterizes the cofree  of spliced arrows, which governs how incomplete morphisms can be nested.
Any  freely generates another category, its contour <cit.>. This can be interpreted as the category that tracks the processes of decomposition that the  describes. The construction is particularly pleasant from the geometric point of view: it takes its name from the fact that it can be constructed by following the contour of the shape of the decomposition (<Ref>).

Contour of a multimorphism.

Let $𝕄$ be a .
Its contour, $\Contour(𝕄)$, is the category presented by
two polarized objects, $X^{∘}$ and $X^{∙}$, for each object $X ∈ 𝕄_{obj}$;

* for each multimorphism $f \in 𝕄(X₁,\dots,Xₙ; Y),$ the following generators,

\begin{align*}
f₀ ፡ Y^{∘} → X₁^{∘};
f₁ ፡ X₁^{∙} → X₂^{∘};
\quad … ; \quad
f_{n-1} ፡ X_{n-1}^{∙} → Xₙ^{∘};
f_{n} ፡ Xₙ^{∙} → Y^{∙};
\end{align*}

with only an $f₀ \colon Y^{∘} → Y^{∙}$ for the case $n = 0$;

* requiring contour to preserve identities, $(\id_{X})₀ = \id_{X^{∘}}$ and $(\id_X)₁ = \id_{X^{∙}}$;

* and requiring contour to preserve compositions, meaning that for each $f ∈ 𝕄(X₁,\dots,Xₙ; Yᵢ)$ and each $g ∈ 𝕄(Y₁,\dots,Yₘ; Z)$, the contour of their composition is defined by the following five cases

$$(f ⨾_{X_i} g)_j = \left\{
\begin{array}{ll}
gⱼ & \mbox{ when } j < i, \\
gᵢ ⨾ f₀ & \mbox{ when } j = i, \\
f_{j-i} & \mbox{ when } i < j < i+n, \\
f_n ⨾ g_{i+1} & \mbox{ when } j = i+n, \\
g_{j-n+1} & \mbox{ when } i+n < j < n + m, \\
\end{array}
\right.$$

with the special case $(f ⨾_{X_i} g)_i = gᵢ ⨾ f₀ ⨾ g_{i+1}$ whenever $n = 0$.

A recent article by Melliès and Zeilberger <cit.> develops the notion of a context-free grammar over a category as a multicategorical functor to the multicategory of spliced arrows. The multicategory of spliced arrows is a universal construction over a category that produces a multicategory of “contexts” over the category.

§.§ Spliced Arrows

The multicatgeory of spliced arrows is formed by arrows containing blanks or holes that could be filled to constuct a morphism. This  gives an algebraic theory of context for the category.

Let $ℂ$ be a category. The  of spliced arrows has objects pairs of objects in $ℂ$, and the multimorphisms are given by sequences of arrows in $ℂ$ separated by $n$ gaps

$$\Splice{ℂ} \left(
\biobj{X₁}{Y₁} , \dots , \biobj{Xₙ}{Yₙ} ;
\biobj{X}{Y}
\right) = ℂ(X;X₁) × \prod_{k=1}^{n-1} ℂ(Y_k, X_{k+1}) × ℂ(Yₙ;Y);$$

which we write as $f₀ ⨾ □ ⨾ \dots ⨾ □ ⨾ fₙ$. That is, the sequence goes from $X$ to $Y$, with holes typed by $\{Xᵢ → Yᵢ\}_{0<i \leq n}$.
Composition is defined by substitution

\begin{align*}
& (f₀ ⨾ □ ⨾ \dots ⨾ □ ⨾ fₙ) ≻_{i} (g₀ ⨾ □ ⨾ \dots ⨾ □ ⨾ gₘ) = \\
& \qquad (g₀ ⨾ □ ⨾ \dots ⨾ gᵢ ⨾ f₀ ⨾ □ ⨾ \dots ⨾ □ ⨾ fₙ ⨾ g_{i+1} ⨾ \dots ⨾ □ ⨾ gₘ),
\end{align*}

and the identity morphism in $\left(\biobj{X}{Y} \right)$ is $id_X ⨾ □ ⨾ id_Y$.

The  of spliced arrows is a .

We will show that dinatural composition is invertible by exhibiting an inverse to the composition operation, up to dinaturality. Consider a spliced arrow $h₀ ⨾ □ \cdots □ ⨾ h_{n+m-1}$ with $(n+m+1)$ holes; we can decompose $n$ of its holes at position $i$ with the following operation.

\begin{align*}
& \decomp_i^n(h₀ ⨾ □ \cdots □ ⨾ h_{n+m-1})  \\
& \qquad = (h₀ ⨾ □ \cdots  hᵢ ⨾ □ ⨾ h_{i+n} \cdots  □ ⨾ h_{n+m-1})\ |\ (\id ⨾ □ ⨾ h_{i+1} \cdots h_{i+n-1} ⨾ □ ⨾ \id) \\
& \qquad = (h₀ ⨾ □ \cdots  \id ⨾ □ ⨾ \id \cdots  □ ⨾ h_{n+m-1})\ |\ (hᵢ ⨾ □ ⨾ h_{i+1} \cdots h_{i+n-1} ⨾ □ ⨾ h_{i+n}).
\end{align*}

This operation is an inverse to dinatural composition. It follows by construction that $(≻)_i ⨾ \decomp_i = \id$, and we now check that $\decomp_i ⨾ (≻)_i$ is an identity up to dinaturality. Let $f₀ ⨾ □  \cdots □ ⨾ fₙ$ and $g₀ ⨾ □  \cdots □ ⨾ gₘ$ be two spliced arrows,

\begin{align*}
& \decomp_i^n((f₀ ⨾ □  \dots □ ⨾ fₙ) ≻_i (g₀ ⨾ □  \dots □ ⨾ gₘ)) \\
& \ =\ \decomp_i^n(g₀ ⨾ □ \dots ⨾ gᵢ ⨾ f₀ ⨾ □ ⨾ \dots □ ⨾ fₙ ⨾ g_{i+1} ⨾ □ \cdots □ ⨾ gₘ)) \\
& \ =\ (g₀ ⨾ \dots ⨾ gᵢ ⨾ f₀ ⨾ □ ⨾ fₙ ⨾ g_{i+1} ⨾ \dots ⨾ gₘ)\ |\ (\id ⨾ □ ⨾ f₁ ⨾ \dots ⨾ f_{n-1} ⨾ □ ⨾ \id) \\
& \ =\ (g₀ ⨾ \dots ⨾ gᵢ ⨾ □ ⨾ g_{i+1} ⨾ \dots ⨾ gₘ)\ |\ (f₀ ⨾ □ ⨾ f₁ ⨾ \dots ⨾ f_{n-1} ⨾ □ ⨾ fₙ).
\end{align*}

We have shown that dinatural composition is invertible.

§.§ Splice-Contour Adjunction

A first explicit account of splice-contour adjunction is due to Melliès and Zeilberger <cit.>. In later  joint work with Earnshaw and Hefford <cit.>, we showed that this adjunction produced not only  but .

Splice is right adjoint to contour.

Let $𝕄$ be a . We will show that any multifunctor to a spliced arrow multicategory, $F ፡ 𝕄 → \Splice{(ℂ)}$, factors through a canonical multifunctor $T ፡ 𝕄 → \Splice(\Contour(𝕄))$ that is followed by a unique functor $F^\sharp ፡ \Contour(𝕄) → ℂ$.
First, we construct  $T ፡ 𝕄 → \Splice(\Contour(𝕄))$, the multifunctor that sends any object $X$ to the pair of polarized objects $\left( \biobj{X^{∘}}{X^{•}} \right)$; and that sends any multimap $f ∈ 𝕄(X₀,\dots,Xₙ;Y)$ to the spliced arrow

$$f₀ ⨾ □ ⨾ \dots ⨾ □ ⨾ fₙ ∈ \Splice(ℂ)\left(\biobj{X_0^{∘}}{X_0^{∙}}, \dots, \biobj{X_n^{∘}}{X_n^{∙}} ; \biobj{Y^{∘}_{\phantom{0}}}{Y^{∙}_{\phantom{0}}}\right).$$

We check now that $T$ is indeed a multifunctor: by construction, it sends $T(f ⨾_{X_i} g) = f ≻_i g$ and it sends $T(\id_X) = (\id_{X^{∘}} ⨾ □ ⨾ \id_{X^{∙}})$.

We will now show that there exists a unique functor $F^\sharp ፡ \Contour{(𝕄)} → ℂ$ factoring the multifunctor $F$, such that $F = T ⨾ \Splice{(F^\sharp)}$. The contour is a category presented by some generators and equations: to define a functor from it, it suffices to define it on the generators and show that it preserves the equations of the presentation. We do so next.
Consider the objects, for each $X ∈ 𝕄_{obj}$, assume $F(X) = \left(\biobj{A}{B}\right)$. We must have that

$$\Splice{(F^\sharp)}(T(X)) = \Splice{(F^\sharp)}\left(\biobj{X^{∘}}{X^{∙}}\right) = \left(\biobj{F^\sharp X^{∘}}{F^\sharp X^{∙}}\right) = \left(\biobj{A}{B}\right),$$

which forces $F^\sharp(X^{∘}) = A$ and $F^\sharp(X^{∙}) = B$. Consider now the morphisms, for each $f \in 𝕄(X₀,\dots,Xₙ;Y)$. We must have that

\begin{align*}
\Splice{(F^\sharp)}(T(f))
= \Splice{(F^\sharp)}(f₀ ⨾ \dots ⨾ fₙ)
= F^\sharp f₀ ⨾ □ ⨾ \dots ⨾ □ ⨾ F^\sharp fₙ,
\end{align*}

which forces $F^\sharp(f_i) = F(f)_i$. This uniquely determines the value of $F^\sharp$ in all of the morphisms of the contour.
We must finally check that that $F^\sharp$ satisfies the equations. We first notice that, by functoriality of $F$, we have

$$F^\sharp((f ⨾_{X_i} g)_j) = F(f ⨾_{X_i} g)_j = (F(f) ⨾_{FX_i} F(g))_j,$$

and, using this and the previous $F^\sharp(f_i) = F(f)_i$, we simply check the five cases of contour composition,

\begin{align*}
F^\sharp((f ⨾_{X_i} g)_j) =
\left\{ \begin{array}{l}
F(g)_j \\
F(g)_i ⨾ F(f)_0 \\
F(f)_{j-i} \\
F(f)_n ⨾ F(g)_{i+1} \\
\end{array}
\right\} =
\left\{ \begin{array}{l}
F^\sharp(gⱼ) \\
F^\sharp(gᵢ) ⨾ F^\sharp(f₀) \\
F^\sharp(f)_{j-i} \\
F^\sharp(f)ₙ ⨾ F^\sharp(g)_{i+1} \\
\end{array}
\right\}.
\end{align*}

This proves the existence of $F^\sharp$, but it also proves that it is the unique possible functor such that $F = T ⨾ \Splice(F^\sharp)$.

§.§ Promonoidal Splice-Contour

We have commented on how any  induces a .
The  of spliced arrows induces a  of spliced arrows.
This  is precisely the one that arises from the adjunction between any category and its opposite category in the monoidal bicategory of profunctors.

The  splice could be seen as a particular case of the more general multicategorical splice.
However, we will see that it is usually better behaved: technically, it is the 2-monoid arising from the 2-duality of a category with its opposite category, $ℂ ⊣ ℂ^{op}$, in the monoidal bicategory of profunctors.
We will not use this particular fact too much, but it will inspire its generalization. In the next chapter, we repeat a monoidal version of the splice-contour adjunction that, by default, uses only the malleable version.

Let $ℂ$ be a category. The  of spliced arrows, $\Splice{ℂ}$, has as objects pairs of objects of $ℂ$. It uses the following profunctors to define morphisms, splits and units.

* $\Splice(ℂ) \left(\biobj{X}{Y} ; \biobj{A}{B} \right) = ℂ(A;X) × ℂ(Y,B);$

* $\Splice(ℂ)( \biobj{X}{Y} ◁ \biobj{X'}{Y'} ; \biobj{A}{B}) = ℂ(A;X) × ℂ(Y;X') × ℂ(Y';B);$

* $\Splice(ℂ)(N ; \biobj{A}{B}) = ℂ(A;B)$.

In other words, morphisms are pairs of arrows $f \colon A \to X$ and $g \colon Y \to B$.
Splits are triples of arrows $f \colon A \to X$, $g \colon Y \to X'$ and $h \colon Y' \to B$. Units are simply arrows $f \colon A \to B$. We use the following notation for

* morphisms, $(f ⨾ □ ⨾ g) ፡ \pbiobj{X}{Y} → \pbiobj{A}{B}$;

* joins, $(f ⨾ □ ⨾ g ⨾ □ ⨾ h) ፡ \pbiobj{X}{Y} ⊲ \pbiobj{X'}{Y'} → \pbiobj{A}{B}$;

* and units, $f ፡ 𝖭 → \pbiobj{A}{B}$.

The contour of a  $ℙ$ is the category $\Contour{(ℙ)}$ presented by two polarized objects, $X^∘$ and $X^•$, for each object $X ∈ ℙ_{obj}$; and generated by the arrows that arise from contouring the decompositions of the .

Contour of a promonoidal category.

Specifically, the contour is the category presented by the following generators, as depicted in <Ref>:

* $a₀ ፡ Y^{∘} → X^{∘}$ and $a₁ ፡ X^{•} → Y^{•}$, for each morphism $a ∈ ℙ(X;Y)$;

* $b₀ ፡ X^{∘} → X^{•}$, for each unit $b ∈ ℙ(N;X)$;

* a triple of generators, $c₀ ፡ Z^{∘} → X^{∘}$, $c₁ ፡ X^{•} → Y^{∘}$ and $c₂ ፡ Y^{•} → Z^{•}$, for each split $c ∈
ℙ(X ⊲ Y; Z)$.

We impose several equations over these generators, all depicted in <Ref>. The equations come from the decomposition of categories and they form the theory of contour.

Theory of contour.

CHAPTER: MONOIDAL CONTEXT THEORY

§ MONOIDAL CONTEXT THEORY

This section develops a theory of context, or incomplete parts, for arbitrary .
In the same way that the theory of context for categories required  or ; the theory of context for  will require  and .

combine a sequential tensor $(⊲)$ with a parallel tensor $(⊗)$; and it is well known that they can be used for process description <cit.>. However, lifting context theory to  will come with a few technical surprises that we develop; the most important one is a normalization monad in the category of : this becomes a crucial step in creating a theory of  that allows incomplete morphisms to take any shape. The morphisms of the  of contexts have been called lenses and combs in the literature, and we characterize them by a universal property.

We revisit the literature on  and normalization in <Ref>.  and their splice-contour adjunction are introduced in <Ref>. We take a technical aside in <Ref> to construct the normalization monad, and we immediately use it in <Ref>.

§ DUOIDAL CATEGORIES

§.§ Duoidal Categories

result from the interaction of two .
By the Eckmann-Hilton argument, each time we have two monoids $(\ast,\circ)$ such that one is a monoid homomorphism over the other, $(a ∘ b) \ast (c ∘ d) = (a \ast c) ∘ (b \ast d)$, we know that both monoids coincide in a single commutative monoid.

However, an extra dimension helps us side-step the Eckmann-Hilton argument. If, instead of equalities or isomorphisms, we use directed morphisms, both monoids (which now may become 2-monoids) do not necessarily coincide, and the resulting structure is that of a .

A duoidal category <cit.> is a category $ℂ$ with two monoidal structures, $(ℂ,⊗, I,α,λ,ρ)$ and $(ℂ,◁, N, β, κ, ν)$ such that the latter distribute over the former.  In other words, it is endowed with a duoidal tensor, $(◁) \colon ℂ × ℂ → ℂ$, together with natural distributors

\begin{align*}
& ψ_2﹕ (X ◁ Z) ⊗ (Y ◁ W) → (X ⊗ Y) ◁ (Z ⊗ W), \\
& ψ_0﹕ I → I ◁ I, \\
& φ_2﹕ N ⊗ N → N, \quad\mbox{and}\\
& φ_0 ﹕ I → N,
\end{align*}

satisfying the following coherence equations (<Ref>, <Ref>).
A duoidal category is strict when both of its monoidal structures are.

In other words, the duoidal tensor and unit are lax monoidal functors for the first monoidal structure, which means that the laxators must satisfy the following equations.

* $(ψ_2 ⊗ id) ⨾ ψ_2 ⨾ (α ◁ α) = α ⨾ (id ⊗ ψ_2) ⨾ ψ_2$, for the associator;

* $(ψ_0 ⊗ id) ⨾ ψ_2 ⨾ (λ ◁ λ) = λ$, for the left unitor; and

* $(id ⊗ ψ_0) ⨾ ψ_2 ⨾ (ρ ◁ ρ) = ρ$, for the right unitor;

* $α ⨾ (id ⊗ φ_2) ⨾ φ_2 = (φ_2 ⊗ id) ⨾ φ_2$, for the associator;

* $(φ_0 ⊗ id) ⨾ φ_2 = λ$, for the left unitor; and

* $(id ⊗ φ_0) ⨾ φ_2 = ρ$, for the right unitor.

§.§ Communication via Duoidals

The operations of a posetal duoidal structure can be interpreted as speaking about the communication of processes <cit.>. Let $(⊗,i)$ and $(⊲,n)$ form a duoidal structure on a poset. We read the elements of this poset as being processes and we interpret

* $x ⊗ y$ as “$x$ and $y$ happen together, in parallel and independently”;

* $x ⊲ y$ as “$y$ happens after $x$, and may depend on it”;

* $i$ as a process that “interrupts communication”;

* $n$ as a process that “does nothing”;

* $x → y$ as “channels of $x$ are included in channels of $y$”.

Under this interpretation, the rules of a  say that

* $(x ⊲ y) ⊗ (z ⊲ w) → (x ⊗ z) ⊲ (y ⊗ w)$, adds intermediate communication;

* $i → i ⊲ i$, allows to interrupt an interrupted process;

* $n ⊗ n → n$, simplifies parallelism that does nothing; and

* $i → n$, allows new communications.

We can already picture this interpretation in terms of communication diagrams. Processes are boxes, and wires represent the information flow: a path from a process to another one means that the first can communicate to the second (<Ref>).

Communication diagrams.

The axioms of a  impose the following transformations of communication diagrams (<Ref>).

We can take these diagrams seriously: they are string diagrams of a monoidal bicategory where processes are endocells. The only structure that we ask of the single object generator is that of an adjoint monoid.

Communication diagram axioms.

§.§ Duoidals via adjoint monoids

Let $(ℂ,⊗,I)$ be a monoidal category; let $(A,\iconwm{},\iconwu{})$ be a monoid and let $(B,\iconbcm{},\iconbcu{})$ be a comonoid. The set of morphisms $ℂ(A;B)$ forms a monoid with the operation of convolution, $f \ast g = \iconbcm ⨾ (f ⊗ g) ⨾ \iconwm$ and the biunit, $e = \iconbcu{} ⨾ \iconwu{}$, as in <Ref>.

Convolution monoid.

Convolution and composition interact duoidally whenever the monoid and the comonoid are adjoint to each other. This is the notion of an adjoint monoid.

An adjoint monoid, in a monoidal bicategory $𝔹$, is an object endowed with both 2-monoid and 2-comonoid structure $(A,\iconwm,\iconwu,\iconwcu,\iconwcm)$, such that the multiplication is adjoint to the comultiplication $(\iconwm ⊣ \iconwcm)$ and the unit is adjoint to the counit $(\iconwu ⊣ \iconwcu)$.

Adjoint monoid.

This means that there exist 2-cells, $ε_{⊗} ፡ \iconwcm ⨾ \iconwm → \id$ and $η_{⊗} ፡ \id → \iconwcm ⨾ \iconwm$, witnessing the adjunction $(\iconwm ⊣ \iconwcm)$; and that there exist 2-cells, $ε_{I} ፡ \iconwcu ⨾ \iconwu → \id$ and $η_{I} ፡ \id → \iconwcu ⨾ \iconwu$ witnessing the adjunction $(\iconwu ⊣ \iconwcu)$, as in <Ref>.

The endocells of an adjoint 2-monoid form a duoidal category with convolution and composition.

Let $(A,\iconwm,\iconwu,\iconwcu,\iconwcm)$ be an , and let $X, Y ∈ 𝔹(A;A)$ be endocells. We define the sequential tensor as the composition, $X ⊲ Y = X \bcomp Y$, with the unit being the identity, $N = \mathbf{I}$. We define the parallel tensor as the convolution, $X ⊗ Y = \iconwcm ⨾ (X \boxtimes Y) ⨾ \iconwm$, with the unit being the pair of monoid units, $I = \iconwcu ⨾ \iconwu$. The duoidal interchangers are constructed out of the 2-cells of the adjoint monoid, taking <Ref> seriously as the string diagrams of a monoidal bicategory.

* The first interchanger, $(X ⊲ W) ⊗ (Y ⊲ Z) → (X ⊗ Y) ⊲ (W ⊗ Z)$, is constructed from the tensor adjunction unit, $η_{⊗} ፡ \id → \iconwm ⨾ \iconwcm$;

* the second interchanger, $I → I ⊲ I$, is constructed from the unit of the unit adjunction, $η_{I} ፡ \id → \iconwu ⨾ \iconwcu$;

* the third interchanger, $I → N$, is constructed from the counit of the unit adjunction, $ε_{I} ፡ \iconwcu ⨾ \iconwu → \id$; and

* the fourth interchanger, $N ⊗ N → N$, is constructed from the tensor adjunction counit, $ε_{⊗} ፡ \iconwcm ⨾ \iconwm → \id$.

Finally, we need to check that all of the structure diagrams commute. This is usually left to the reader <cit.>; we can visualize the equations as surface diagrams.

A particular case is the convolution of two parallel profunctors $P, Q ፡ ℂ → 𝔻$ between monoidal categories. A monoidal category determines an adjoint monoid in the monoidal bicategory of profunctors. Convolution is the operation that constructs a profunctor $P \ast Q ፡ ℂ → 𝔻$ defined by

$$(P \ast Q)(A,B) = {\textstyle ∫}^{X,X',Y,Y'} ℂ(A, X ⊗ Y) × P(X,X') × Q(Y,Y') × 𝔻(X'⊗Y',B).$$

Whenever we particularize to presheaves over a monoidal category $ℂ$, we recover Day convolution of presheaves.

$$(F \ast G)(A) = {\textstyle ∫}^{X,Y} ℂ(A, X ⊗ Y) × F(X) × G(Y).$$

In particular, the endoprofunctors over any  form a , this is the duoidal category that we study in <Ref>.

§.§ Be Careful with Duoidal Coherence

possess a coherence theorem that determines that any two parallel morphisms constructed out of structure isomorphisms commute. In contrast,  do not satisfy that same statement. This causes some confusion around coherence for . I bring an example of how this confusion may arise, hoping that it will help the interested reader and that it may further justify the importance of expository category theory.

We could be tempted to provide an alternative definition of  that avoids asking for a bunch of commutative diagrams by simply asking that any formal such diagram commutes. In fact, this may possible for the  studied by Spivak and Shapiro <cit.>, who comment that

alternatively, duoidal categories can be defined by the two monoidal structures along with the generating structure maps [...] (4) natural in $a, b, c, d$ which satisfy equations guaranteeing that any two structure maps built from those in (4) between the same two expressions in $y_{⊗} , y_{⊲} , ⊗, ⊲$ are equal.

One of the first, most complete and comprehensive accounts of  is the monograph by Aguiar and Mahajan <cit.>. It includes a passing comment that could suggest that this version can be proven correct. It says that

“[...] if two morphisms $A → B$ are constructed out of the structure maps in $ℂ$ (including the structure constraints of the monoidal categories $(ℂ, \diamond, I)$ and $(ℂ, \star, J)$), then they coincide.”

However, intepreted literally and strictly, this turns out to not be true. Two parallel morphisms constructed out of the structure maps of a  do not need to coincide.

There exist two different maps of type $I ⊲ I → I$ constructed out of the structure maps of a .

We can consider two maps of type $I ⊲ I → I$, depending on which of the two parallel units we decide to convert to a sequential unit using the laxators. Explicitly, we are saying that $(I ⊲ φ_0) ⨾ ρ_{⊲}$ and $(φ_0 ⊲ I) ⨾ λ_{⊲}$ do not coincide; and the more intuitive string diagrams for bicategories for  confirm this (<Ref>). We will construct an explicit example of this phenomenon.

Bicategorical string diagrams for the two coherence maps.

Consider the  of endoprofunctors over a . This is one of the first examples of  described by Street <cit.>; it is also described by Garner and López Franco <cit.>, even when the axioms are not explicitly checked in print.
In this category of endoprofunctors over $ℂ$,  parallel tensor is the profunctor
$I(X;Y) = ℂ(X;I) × ℂ(I;Y)$, and sequencing two of them gives

\[(I ⊲ I)(X;Y) = \hom(X;I) × \hom(I;I) × \hom(I;Y).\]

In this case, the two maps send the triple $(f,a,g)$ to $(f ⨾ a, g)$ and $(f, a ⨾ g)$, respectively. However, these two pairs do not need to be equal if $a ∈ \hom(I;I)$ is a non-identity morphism.

[Graded spaces]
We look for a more classical source of examples in the theory of graded spaces.
Let $(𝕍,⊗,I)$ be a  with coproducts that are preserved by the tensor; let $(G,+,0)$ be a commutative monoid. We say that the functor category $[G,𝕍]$ is the category of $G$-graded $𝕍$-spaces. This category has a rich structure; we highlight two of its tensor products: the pointwise or Hadamard tensor product

\[(V ⊗ W)ₙ = Vₙ ⊗ Wₙ,\mbox{ for each } n ∈ G,\mbox{ with unit }𝕀ₙ = I;\]

and the convolution or Cauchy tensor product

\[(V • W)ₙ = \sum\nolimits_{k+m = n} Vₖ ⊗ Wₘ, \mbox{ with unit } \mathbf{1}ₙ = \mathbf{0}\mbox{ except for }\mathbf{1}₀ = I.\]

These two tensors interact in a  with a laxator as follows; see for instance the work of López Franco and Vasilakopoulou <cit.>.

\[\sum_{k+m = n} Vₖ ⊗ Wₖ ⊗ Uₘ ⊗ Zₘ → \left( \sum_{k₁ + m₁ = n₁} V_{k₁} ⊗ U_{m₁} \right) ⊗ \left( \sum_{k₂ + m₂ = n₂} W_{k₂} ⊗ Z_{m₂} \right).\]

Dually, there exist two different maps of type $J → J ⊗ J$ constructed out of the structure maps of a .

This follows from the previous <Ref>, by considering the opposite . However, let us comment a second example <cit.>. Consider the  of graded spaces over a monoid $G$. The two maps, $𝕀 → 𝕀 ⊗ 1 → 𝕀 ⊗ 𝕀$ and $𝕀 → 1 ⊗ 𝕀 → 𝕀 ⊗ 𝕀$, correspond to inclusions of the vector space graded by $g ∈ G$ into the summand indexed by $(g,0)$ or $(0,g)$, respectively; these are different in general.

In fact, the stronger statement of coherence does not seem to be used explicitly in any of these two texts, and the definition of  as completely coherent strucutres is not usually found in the literature. Most authors, like Aguiar and Mahajan <cit.>, and Garner and López Franco <cit.>, revert to the definition of  as a 2-monoid in the monoidal bicategory of monoidal categories.

Aguiar and Mahajan <cit.> do actually point out that the expected coherence theorem should follow from the coherence theorem for lax monoidal functors. The confusion can arise if we do not realize that this coherence theorem does not actually prove that any two parallel maps coincide: in particular, coherence for lax monoidal functors does not prove that the two maps $F(I) ⊗ F(I) → F(I)$ coincide. In this case, however, the problem is better known – it is mentioned by Malkiewich and Ponto <cit.>, who cite a short mention in the original proof by Lewis <cit.> and Kelly and Laplaza <cit.>.

§.§ Bibliography

I thank Marcelo Aguiar and Swapneel Mahajan <cit.> for their generosity, helping me confirm the problem and specially for providing the second counterexample; I thank Brandon Shapiro and David Spivak for helping me follow this same idea on their work. I thank Matt Earnshaw for sharing his knowledge of the literature on .

§ NORMAL DUOIDAL CATEGORIES

seem to contain too much structure: of course, we want to split things in two different ways, sequentially $(◁)$ and in parallel $(⊗)$; but that does not necessarily mean that we want to keep track of two different types of units, parallel $(I)$ and sequential $(N)$. The atomic components of our decomposition algebra could be the same, without having to care if they are atomic for sequential composition or atomic for parallel composition; when this is the case, we talk of normal duoidal categories.

A normal duoidal category is a  in which the map $φ_0 ፡ I → N$ is an isomorphism.

While  are useful to track communication between processes; symmetric normal duoidal categories track dependencies – whether a process' input depends on the output of another – structuring a dependency poset. This idea is explored by Garner and López Franco <cit.> and Spivak and Shapiro <cit.>, and it has a formal counterpart in <Ref>.

Most  we have seen so far – and particularly those arising from  – have two different units.
There exists a well-known abstract procedure that, starting from some , constructs a new  that is normal: both units are identified. This procedure is known as normalization, and it can only be applied to  with certain coequalizers preserved by the tensor.

§.§ Normalization of duoidal categories

Garner and López Franco construct the normalization of a well-behaved , using a new duoidal category of bimodules <cit.>.

Let $M$ be a bimonoid in the  $(𝕍,⊗,I,◁,N)$, with maps $e ﹕ I → M$ and $m ﹕ M ⊗ M → M$; and with maps $u ﹕ M → N$ and $d ﹕ M → M ◁ M$. Consider now the category of $M^⊗$-bimodules. This category has a monoidal structure lifted from $(𝕍,◁,N)$:

* the unit, $N$, has a bimodule structure with

$$M⊗N⊗M \overset{u ⊗ \id ⊗ u}\longrightarrow  N⊗N⊗N \longrightarrow N;$$

* the sequencing of two $M^⊗$-bimodules is a $M^⊗$-bimodule with

M&⊗(A◁B)⊗M \\
&→ (M◁M)⊗(A◁B)⊗(M◁M) \\
&→ (M⊗A⊗M)◁(M⊗B⊗M) → A◁B.
\end{aligned}$$

Moreover, whenever $𝕍$ admits reflexive coequalizers preserved by $(⊗)$, the category of $M^{⊗}$-bimodules is monoidal with the tensor of bimodules: the coequalizer

$$A ⊗ M ⊗ B \rightrightarrows A ⊗ B \twoheadrightarrow A ⊗_M B.$$

In this case $(\mathbf{Bimod}^{⊗}_M, ⊗_M, M, ◁, N)$ is a .

Let $(𝕍,⊗,I,◁,N)$ be a  with reflexive coequalizers preserved by $(⊗)$. The category of $N$-bimodules is then a ,

$$\mathcal{N}(𝕍) = (\mathbf{Bimod}^{⊗}_N, ⊗_N, N, ◁, N).$$

We call this category the normalization of the  $𝕍$.

§.§ Physical duoidal categories

The interaction of dependent and independent composition of  is a recurrent idea in physical models: categorical models of spacetime exhibit this structure <cit.>; but it is also exhibited by parallel and sequentially composing programs <cit.>; or more simply, by the category of partially ordered sets.

In most of these cases, the  has an extra property: the parallel tensor ($⊗$) is symmetric. This is what motivates the name physical duoidal category for the $⊗$-symmetric .

A physical duoidal category is a  endowed with a  structure for its parallel tensor.

Posets are a canonical example of a : in fact, it is known that a subcategory of the category of posets and poset inclusions forms the free  over a generator. In that precise sense, duoidal expressions are dependency tracking posets.

The category of poset shapes, $\mathbf{PosetSh}$, is the skeleton of the category of finite posets with bijective-on-objects monotone functions. Objects are isomorphism classes of finite posets, and morphisms are inclusions.

Poset shapes form a .

The sequential tensor is constructed by sequentially joining the posets. Let $(P, ≤_{P})$ and $(Q, ≤_{Q})$ be two posets; their sequentiation, $P ⊲ Q$, is a poset that contains a copy of $P$, a copy of $Q$, and an edge $pᵢ ≤ qⱼ$ for each $pᵢ ∈ P$ and $qⱼ ∈ Q$; that is,

$$P ⊲ Q = (P + Q, ≤_P + ≤_Q + \{ pᵢ ≤ qⱼ \mid pᵢ ∈ P, qⱼ ∈ Q\}).$$

The parallel tensor, $P ⊗ Q$, is defined to be the disjoint union of posets,
$P ⊗ Q = (P + Q, ≤_P + ≤_Q)$, which defines a symmetric monoidal structure. The empty poset is the unit for both sequential and parallel tensoring, making $\mathbf{PosetSh}$ a .

The category of poset shapes is not posetal: there are, for instance, two possible inclusions of the discrete two-element poset into itself. This prompts us to label the nodes to indicate inclusions, as in <Ref>, but we work up to relabelling, or $α$-equivalence.

Poset inclusion.

What makes this  particularly relevant is that it contains the free  over a generator. Every formal normal duoidal expression constructs a poset: we simply substitute each variable by the singleton poset and we interpret the expression in the  of poset shapes. Every formal structure map between normal duoidal expressions corresponds to an inclusion; for instance, <Ref> documents the structure map $(p ⊲ q) ⊗ (r ⊲ s) → (p ⊗ r) ⊲ (q ⊗ s)$.

Formalizing this result needs a bit of care, though: while all formal physical duoidal expressions correspond to posets, not every poset shape corresponds to a physical duoidal expression. The poset shapes that arise from applying duoidal operations to the singleton poset are called expressible, and we have a characterization result for them.

Expressible poset shapes are those inductively constructed from

* the empty poset, $𝖭$;

* the singleton poset, $\{A\}$;

* the union of posets, $P ⊗ Q = (P + Q, ≤_P + ≤_Q)$; and

* the sequencing of posets,
$$P ⊲ Q = (P + Q, ≤_P + ≤_Q + \{ pᵢ ≤ qⱼ \mid pᵢ ∈ P, qⱼ ∈ Q\}).$$

Expressible poset shapes form a full duoidal subcategory of the  of poset shapes, $\mathbf{ExprSh}$.

Not every poset shape is expressible. In fact, a poset shape is not expressible if and only if it admits an inclusion of the Z-poset shape defined by <Ref>.

The Z poset shape.

The  $\mathbf{ExprSh}$ of expressible poset shapes is the free  on a single object. There exists exactly one structure map between any two objects of the free  for each inclusion of their associated expressible posets.

Coherence for  needs some care: not any two morphisms between distinctly-typed expressions in the free  are equal (<Ref>). However, the previous theorem implies that the same statement is true for .

Any two morphisms between distinctly typed expressions in the free  over a set of objects are equal.

§.§ Physical Lax Tensor of a Physical Duoidal Category

Let us recap our interpretation of : they track an underlying poset of dependencies. The sequential tensor, $X ⊲ Y$, says that $X$ occurs before $Y$, but $Y ⊲ X$ says that $Y$ occurs before $X$; consequently, it is not symmetric. The parallel tensor, $X ⊗ Y$, states that both $X$ and $Y$ occur independently. This final section of our introduction to  shows what happens when we want to consider both $X$ and $Y$ but we do not know at all how they interact: the tensor that tracks this case is a derived operation, the physical tensor, $X \boxtimes Y$.

The physical tensor simply says that both occur at some point: it does not impose independence, but it does not impose any particular dependency either. The physical tensor $X \boxtimes Y$ says that $X$ may occur before $Y$, or $Y$ before $X$, or both in parallel and in that case it does not matter how we regard the dependency. This is a tool that we will employ later to discuss a version of monoidal context that does not track dependency: wiring diagrams (<cit.>, <Ref>).

The binary physical tensor, $X \boxtimes Y$, is easy to define: it is the pushout of the two structure maps $X ⊗ Y → X ⊲ Y$ and $X ⊗ Y → Y ⊲ X$. However, unlike most tensors, its n-ary version cannot be deduced from its binary and nullary versions; the physical tensor is only a lax tensor.

A lax monoidal category is a category $ℂ$ endowed with a family of lax tensor n-fold tensor functors $(\boxtimes) ፡ ℂ^{n} → ℂ$ – written as $X₁ \boxtimes … \boxtimes Xₙ$, with the 0-ary case $E$ – and a family of associator natural transformations that unbias the application of the lax tensor,

$$α ፡ \boxtimes_{i = 0}^{n} \left( \boxtimes_{j = 0}^{k_i} X^{i}_{j} \right) → X_{1}^{1} \boxtimes … \boxtimes X^{1}_{k_1} \boxtimes … \boxtimes X^{n}_1 \boxtimes … \boxtimes X^n_{k_n},$$

such that all formally well-typed equations hold.

Let $(ℂ,⊗,I,⊲,N)$ be a .
The physical tensor, $(\boxtimes)$, is an additional lax monoidal tensor, defined as the glueing of the sequential tensor $(⊲)$ along the parallel tensor $(⊗)$; that is, it is the pushout on the following family of structure maps, indexed by permutations

$$l_{σ} ፡ X₁ ⊗ … ⊗ Xₙ → X_{σ1} ⊲ … ⊲ X_{σn},\mbox{ for } σ ∈ P(n).$$

This only forms a lax tensor for a good reason. Consider the simpler case of three elements, $X \boxtimes Y \boxtimes Z$. This expression allows all of the possible six permutations to occur: (i) $X ⊲ Y ⊲ Z$; (ii) $X ⊲ Z ⊲ Y$; (iii) $Y ⊲ X ⊲ Z$; (iv) $Y ⊲ Z ⊲ X$; (v) $Z ⊲ X ⊲ Y$; and (vi) $Z ⊲ Y ⊲ X$. However, when we consider $(X \boxtimes Y) \boxtimes Z$, we are only allowing a certain subset of these cases to occur. Namely, only those where $Z$ does not happen between $X$ and $Y$: (i) $X ⊲ Y ⊲ Z$; (ii) $Y ⊲ X ⊲ Z$; (iii) $Z ⊲ X ⊲ Y$; and (iv) $Z ⊲ Y ⊲ X$.
This is why the physical tensor is only lax. We have two inclusions:
$(X \boxtimes Y) \boxtimes Z → X \boxtimes Y \boxtimes Z$ and  $X \boxtimes (Y \boxtimes Z) → X \boxtimes Y \boxtimes Z$,
but these are not isomorphisms.

The physical tensor defines a lax monoidal structure. Given any  $(ℂ,⊗,⊲,N)$, the physical tensor defines a lax monoidal category $(ℂ,\boxtimes,N)$.

The definition of the laxator follows from the universal property of the pushout; the coherence equations hold by uniqueness of the maps constructed out of this universal property.

§.§ Bibliography

The original monograph on  is due to Aguiar and Mahajan <cit.> –  were originally known as “2-monoidal categories”; Street first described multiple examples that we recall <cit.>, and Garner and López Franco mention for the first time the connection to  <cit.>. The reason  do not have a correspondence in lower dimensional algebra is the Eckmann-Hilton argument <cit.>.

follow the definition and nomenclature of Spivak and Shapiro <cit.>; their work makes the case for interpreting them as expressing dependencies between processes and argues initiality of the category of expressible posets. It seems originally due to Grabowski <cit.> that expressible posets are precisely those not containing a Z, and Gischer recognized the lax interchange of  as subsumption of posets <cit.>. Even if the physical lax tensor does not seem to appear in the related literature, its definition and its consideration as a lax tensor follow the work of Leinster <cit.> and the abstraction of commutativity by Garner and López Franco <cit.>. I thank Matt Earnshaw for multiple pointers to the literature.

§ PRODUOIDAL DECOMPOSITION OF MONOIDAL CATEGORIES

§.§ Produoidal categories

, first defined by Booker and Street <cit.>, provide an algebraic structure for the interaction of sequential and parallel decomposition. A  $𝕍$ not only contains morphisms, $𝕍(X; Y)$, as in a category, but also sequential joints, $𝕍(X_0 ◁ X_1; Y)$,  and sequential units, $𝕍(N; X)$, provided by a  structure; and parallel joints, $𝕍(X_0 ⊗ X_1; Y)$ and parallel units, $𝕍(I; X)$, provided by another  structure.

These splits must be coherent. For instance, imagine we want to join  $X_0$, $X_1$ and $X_2$ (sequentially) into $Y$. Joining $X₀$ and $X₁$ into something $(•)$, and then joining that something with $X_2$ to produce $Y$ should be doable in essentially the same ways as joining $X₁$ and $X₂$  into something $(•)$, and then joining that something with $X_0$ to produce $Y$. Formally, we are saying that

$$𝕍(X_0 ⊲ X₁ ; •) ⋄ 𝕍(• ⊲ X_2; Y) ≅ 𝕍(X₁ ⊲ X₂ ; •) ⋄ 𝕍(X₀ ⊲ • ; Y),

and, in fact, we just write $𝕍(X_0◁ X_1 ◁ X_2; Y)$ for the set of such transformations. This is precisely what we ask for in a  structure.

A produoidal category is a category $𝕍$ endowed with two  structures,

𝕍(• ⊗ • ; •) ፡ 𝕍 × 𝕍 → 𝕍, \mbox{ and } 𝕍(I; •) ፡ 1 → 𝕍, \\
𝕍(• ◁ • ; •) ፡ 𝕍 × 𝕍 → 𝕍, \mbox{ and } 𝕍(N; •) ፡ 1 → 𝕍,
\end{gathered}$$

such that one laxly distributes over the other.
This is to say that it is endowed with the following natural lax interchangers:

* $ψ_2 ፡ 𝕍((X◁Y)⊗(Z◁W);•) → 𝕍((X⊗Z)◁(Y⊗W);•)$,

* $ψ_0 ፡ 𝕍(I;•) → 𝕍(I◁I;•)$,

* $φ_2 ፡ 𝕍(N⊗N;•) → 𝕍(N;•)$, and

* $φ_0 ፡ 𝕍(I;•) → 𝕍(N;•)$.

Interchangers, together with unitors and associators, must satisfy coherence conditions (see <Ref>). We denote by $\pDuo$ the category of  and .

Let $𝕍$ be a , then its category of copresheaves, $[𝕍,\Set]$, is a .

Notation for nesting functorial structures, say $(◁)$ and $(⊗)$, is straightforward: we use expressions like $(X_1 ⊗ Y_1) ◁ (X_2 ⊗ Y_2)$ without a second thought. Nesting the profunctorial (or virtual) structures $(⊲)$ and $(⊗)$ is more subtle: defining $𝕍(X ⊗ Y; •)$ and $𝕍(X ◁ Y; •)$ for each pair of objects $X$ and $Y$ does not itself define what something like $𝕍((X_1 ⊗ Y_1) ◁ (X_2 ⊗ Y_2); •)$ means. Recall that, in the profunctorial case, $X_1 ◁ Y_1$ and $X_1 ⊗ Y_1$ are not objects themselves: they are just names for the  $𝕍(X_1 ◁ Y_1; •)$ and $𝕍(X_1 ⊗ Y_1; •)$, which are not representable.

Instead, when we write $𝕍((X_1 ⊗ Y_1) ◁ (X_2 ⊗ Y_2); •)$, we formally mean the composition of  $𝕍(X_1 ⊗ Y_1; •_1) ⋄ 𝕍( X_2 ⊗ Y_2; •_2) ⋄ 𝕍(•_1 ◁ •_2 ; •)$. By convention, nesting profunctorial structures means  composition in this text.

Should we reverse the direction of the interchangers? Depending on the author,  and  are reversed. It seems that both conventions have their advantages. The one we follow here <cit.> makes intuitive sense: it follows the multicategorical and operadic point of view – multiple ingredients produce a result. The opposite one <cit.> gets the interchangers to be those of a  and it becomes clear that there is a correspondence between  and closed  on preshaves.

§.§ Monoidal Contour of a Produoidal Category

Any  freely generates a monoidal category, its monoidal contour. Contours form a monoidal category of paths around the decomposition trees of the .
Contours follow a pleasant geometric pattern where we follow the shape of the decomposition, both in the parallel and sequential dimensions, to construct both sequential and parallel compositions for a monoidal category.

The contour of a  $𝔹$ is the  $\mContour{𝔹}$ presented by two polarized objects, $X^{∘}$ and $X^{•}$, for each object $X ∈ 𝔹_{\text{obj}}$; and generated by arrows that arise from contouring both sequential and parallel decompositions of the .

Generators of the monoidal category of contours.

Specifically,  is the  presented by the following generators in <Ref>:

* $a_0 ፡ Y^{∘} → X^{∘}$ and $a_1 ፡ X^{•} → Y^{•}$, for each morphism $a ፡ X → Y$;

* $b_0 ፡ X^{∘} → X^{•}$, for each , $b ፡ 𝖭 → X$;

* $c_0 ፡ X^{∘} → I$ and $c_1 ፡ I → X^{•}$, for each , $c ፡ I → X$;

* a triple of generators $d_0 ፡ Z^{∘} → X^{∘}$, $d_1 ፡ X^{•} → Y^{∘}$ and $d_2 ፡ Y^{•} → Z^{•}$, for each  $d ፡ X ⊲ Y → Z$; and

* a pair of generators $e_0 ፡ Z^{∘} → X^{∘} ⊗ Y^{∘}$ and $e_1 ፡ X^{•} ⊗ Y^{•} → Z^{•}$ for each , $e ፡ X ⊗  Y → Z$.

We impose all the equations of the theory of contour. Additionally, we also impose all of the equations depicted in <Ref>. Together, these form the theory of , which adds to the theory of sequential contour a new monoidal dimension.

Extra equations for the theory of monoidal contour.

extends to a functor

$$\mContourF : \pDuo → \MonCat{}.$$

<Ref> defines how the functor acts on objects. We define the action on , the morphisms of the category of . Given a , $F: 𝕍 → 𝕎$, let us define the strict monoidal functor $\mContour{F} : \mContour{𝕍} → \mContour{𝕎}$ by the following morphism of generators:

* objects $X^{∘}$ and $X^{•}$ are mapped to $F(X)^{∘}$ and $F(X)^{•}$;

* for each $a ፡ X → Y$, the morphisms $a_0 : X^{∘} → X^{∘}, a_1 : X^{•} → Y^{•}$ are mapped to $F(a)_0$ and $F(a)_1$;

* for each $b ፡ I → X$, both $b_0 : X^{∘} → I$ and $b_1 : I → X^{•}$ are mapped to $F_I(b)_0$ and $F_I(b)_1$;

* for each $c ፡ 𝖭 → X$, the morphism $c_0 : X^{∘} → X^{•}$ is mapped to $F_{𝖭}(c)_0$;

* for each $d ፡ X ⊲ Y → Z$, the morphisms $d_0 : Z^{∘} → X^{∘}$, $d_1 : X^{•} → Y^{∘}$ and $d_2 : Y^{•} → Z^{•}$ are mapped to $F_{◁}(d)_0$, $F_{◁}(d)_1$ and $F_{◁}(d)_2$;

* for each $e ፡ X ⊲ Y → Z$, the morphisms $e_0 : Z^{∘} → X^{∘} ⊗ Y^{∘}$, and $e₁ : X^{•} ⊗ Y^{•} → Z^{•}$ are mapped to $F_{⊲}(e)_0$, and $F_{◁}(e)₁$.

To show that this defines a morphism of presentations, we need to prove that the assignment of generators preserves the equations of the theory of contour, in <Ref>. Because $F: 𝕍 → 𝕎$ is a , the images of the generators do satisfy all of the contour equations of the target category. As a consequence, this assignment extends to a strict monoidal functor.

Finally, when $\id{_𝕍} : 𝕍 → 𝕍$ is an identity, the resulting functor is an identity because it is the identity on generators. Let $G : 𝕌 → 𝕍$ be another , then $\mContour{G⨾F} = \mContour{G}⨾ \mContour{F}$ follows from the composition of .

§.§ Produoidal Splice of a Monoidal Category

We want to go the other way around: given a , what is the  that tracks the decomposition of arrows in that ?
This subsection finds a right adjoint to the  construction: the  of spliced monoidal arrows.

Spliced monoidal arrows.

Let $(ℂ,⊗,I)$ be a .
Its  of spliced monoidal arrows, $\mSplice{ℂ}$, has objects formed by pairs, $\mSplice{ℂ}_{obj} = (ℂ^{op} × ℂ)_{obj}$, and is defined by the following profunctors, depicted in <Ref>.

* $\mSplice{ℂ} \left(\biobj{X}{Y} ;\biobj{A}{B} \right) = ℂ(A;X) × ℂ(Y,B)$,

* $\mSplice{ℂ}(\biobj{X}{Y} ◁ \biobj{X'}{Y'}; \biobj{A}{B}) = ℂ(A;X) × ℂ(Y;X') × ℂ(Y';B);$

* $\mSplice{ℂ}( \biobj{X}{Y} ⊗ \biobj{X'}{Y'}; \biobj{A}{B}) = ℂ(A;X ⊗ X') × ℂ(Y ⊗ Y';B);$

* $\mSplice{ℂ}(𝖭; \biobj{A}{B};) = ℂ(A;B);$

* $\mSplice{ℂ}(I; \biobj{A}{B}) = ℂ(A;I) × ℂ(I;B)$.

indeed form a .

The complete proof constructs all of the necessary natural isomorphisms using coend calculus. We refer to joint work of this author with Earnshaw and Hefford, where the equations are proven in full detail <cit.>.

The produoidal algebra of spliced arrows is a natural construction: abstractly, we know that there exists a duoidal structure on the endomodules of any monoidal category <cit.> – monoidal spliced arrows form its explicitly constructed produoidal counterpart.
What may be more surprising is that spliced arrows have themselves a universal property as part of an adjunction.

form a  with their linkProduoidalComponentssequential and parallel splits, units, and suitable coherence morphisms and laxators.  extend to a functor $\mSpliceF{} : \MonCat → \pDuo$.
The  and the  are left and right adjoints to each other, respectively.

Monoidal contour $\mContour{𝔹}$ is presented by generators and equations: to specify a strict monoidal functor $\mContour{𝔹} → 𝕄$, it is enough to specify images of the generators and then prove that they satisfy the equations.

Let $(𝕄,⊗_M,I_M)$ be a . Then a strict monoidal functor $\mContour{𝔹} → 𝕄$ amounts to the following data satisfying some extra conditions.

* For each object $X \in \obj{𝔹}$, a pair of objects $X^{∘}, X^{•} ∈ \obj{𝕄}$;

* for each element $f ፡ 𝖭 → X$, a morphism $f_0 ፡ X^{∘} → X^{•}$;

* for each unit $f ፡ I → X$, a choice of $f_0 ፡ X^{∘} → I$ and $f_1 ፡ I → X^{•}$;

* for each morphism $f ፡ X → Y$, a choice of $f_0 ፡ Y^{∘} → X^{∘}$ and $f_1 ፡ X^{•} → Y^{•}$;

* for each sequential split $f ፡ X ⊲ Y → Z$, a choice of morphisms $f_0 ፡ Z^{∘} → X^{∘}$, plus $f_1 ፡ X^{•} → Y^{∘} \mbox{ and } f_2 ፡ Y^{•} → Z^{•}$;

* for each parallel split $f ፡ X ⊗ Y → Z$, a choice of morphisms $f_0 ፡ Z^{∘} → X^{∘} ⊗ Y^{∘}\mbox{ and }f_1 ፡ X^{•} ⊗ Y^{•} → Z^{•}$.

In order to construct a well-defined strict monoidal functor, the previous assignments must satisfy the following conditions for each one of the two :

* $α(a ⨾_1 b) = (c ⨾_2 d)$ in the  implies $a_0 ⨾ (b_0 ⊗ \id) = c_0 ⨾ (\id ⊗ d_0)$ and $(b_1 ⊗ \id) ⨾ a_1 = (\id ⊗ d_1) ⨾ c_1$ in the ;

* $λ(a ⨾_1 b) = c = ρ(d ⨾_2 e)$ in the  implies $a_0 ⨾ (b_0 ⊗ \id) = c_0 = d_0 ⨾ (\id ⊗ e_0)$ and  $(b_1 ⊗ \id) ⨾ a_1 = c_1 = (\id ⊗ e_1) ⨾ d_1$ in the ;

Moreover, they must also satisfy the following conditions for the .

* $ψ_2(a ｜ b ｜ c) = (d ｜ e ｜ f)$ in the  implies $a_0 ⨾ (b_0 ⊗ c_0)  = d_0 ⨾ e_0, b_1 ⊗ c_1 = e_1 ⨾ d_1 ⨾ f_0$ and $(b_2 ⊗ c_2) ⨾ a_1 = f_1 ⨾ d_2$ in the ;

* $ψ_0(a) = (b ｜ c ｜ d)$ in the  implies $a_0 = b_0 ⨾ c_0$, $\id = c_1 ⨾ b_1 ⨾ d_0$, and $a_1 = d_1 ⨾ b_2$ in the ;

* $φ_2(a ｜ b ｜ c) = d$ in the  implies $a_0 ⨾ (b_0 ⊗ c_0) ⨾ a_1 = d_0$ in the ;

* $φ_0(a) = b$ in the  implies $a_0 ⨾ a_1 = b_0$ in the .

On the other hand, a  $𝔹 \to \mSplice{𝕄}$, also amounts to the following data. We will state it in multiple points and finally confirm that each one of these points has a correspondence on the first part of the proof, finishing the definition.

* For each object $X \in \obj{𝔹}$, an object $(X^{∘}, X^{•}) \in \obj{\mSplice{𝕄}}$;

* for each element $f ፡ 𝖭 → X$, a morphism $f_0 ፡  𝖭 → \pbiobj{X^{∘}}{X^{•}};$

* for each unit, $f ፡ I → X$, a unit $⟨ f_0 \parallel f₁ ⟩ ፡ I → \pbiobj{X^{∘}}{X^{•}}$;

* for each morphism $f ፡ X → Y$, a splice $\bisplice{f_0}{f_1} ፡ \pbiobj{X^{∘}}{X^{•}} → \pbiobj{Y^{∘}}{Y^{•}}$;

* for each seq. join $f ፡ X ⊲ Y → Z$, a spliced arrow

$$\trisplice{f_0}{f_1}{f_2} ፡ \pbiobj{X^{∘}}{X^{•}} ⊲ \pbiobj{Y^{∘}}{Y^{•}} → \pbiobj{Z^{∘}}{Z^{•}};$$

* for each par. join $f ፡ X ⊗ Y → Z$, a spliced arrow

$$⟨ f_0 ⨾ □ ⊗ □ ⨾ f_1 ⟩ ፡ \pbiobj{X^{∘}}{X^{•}} ⊗ \pbiobj{Y^{∘}}{Y^{•}}→ \pbiobj{Z^{∘}}{Z^{•}}.$$

The following conditions must hold for each one of the . These correspond definitionally to the conditions for the two promonoidal structures we imposed before.

* $α(a ｜ b) = (c ｜d)$ in the  implies $α(Fa ｜Fb) = (Fc ｜ Fd)$ for the spliced arrows;

* $λ(a ｜ b) = c = ρ(d ｜ e)$ in the  implies $λ(Fa ｜ Fb) = Fc = ρ(Fd ｜ Fe)$ for the spliced arrows.

Finally, all the following conditions must also hold for the . These are definitionally equal to the conditions for the  we imposed before.

* $ψ_2(a ｜ b ｜ c) = (d ｜ e ｜ f)$ in the  implies
$$ψ_2(Fa ｜ Fb ｜ Fc) = (Fd ｜Fe ｜Ff);$$

* $ψ_0(a) = (b ｜ c ｜ d)$ in the  implies
$$ψ_0(Fa) = (Fa ｜ Fc ｜ Fd);$$

* $φ_2(a ｜ b ｜ c) = d$ in the  implies
$$φ_2(Fa ｜Fb ｜ Fc) = Fd;$$

* $φ_0(a) = b$ in the  implies $φ_0(Fa) = Fb$.

Each of these points is exactly equal by definition to the relative point in the first part of the proof: this establishes the desired adjunction. In other words, the definition of monoidal splice is precisely the one that makes this proof hold definitionally – even when we gave multiple different characterizations of it.

§.§ A Representable Parallel Structure

A  has two tensors, and neither is, in principle, representable. However, the cofree  over a category we have just constructed happens also to have a representable tensor, $(⊗)$: spliced monoidal arrows form a .

This means $\mSplice{ℂ}$ has the structure of a virtual duoidal category <cit.> or monoidal multicategory, defined by Aguiar, Haim and López Franco <cit.> as a pseudomonoid in the cartesian monoidal 2-category of multicategories.

and  of spliced monoidal arrows are representable . Explicitly,

\begin{align*}
& \mSplice{ℂ}\left( \biobj{X}{Y} ⊗ \biobj{X'}{Y'}; \biobj{A}{B}\right) ≅
\mSplice{ℂ}\left( \biobj{X ⊗ X'}{Y ⊗ Y'} ; \biobj{A}{B}\right),
\mbox{ and } \\
& \mSplice{ℂ}\left( I ; \biobj{A}{B}\right) ≅
\mSplice{ℂ}\left( \biobj{I}{I} ; \biobj{A}{B} \right).
\end{align*}

In fact, these sets are equal by definition. However, we argue that there is a reason to work in the full generality of : produoidal categories can always be normalized.

Normalization is a procedure to mix both tensors of a duoidal category, $(⊗)$ and $(\triangleleft)$, but not every  has a normalization <cit.>.
It is folklore that one loses nothing by regarding non-representable produoidal structures as representable duoidal structures on presheaves, dismissing that they are moreover closed <cit.>; thus, one would expect only some produoidal categories to be normalizable – after all, only some duoidal categories are.
Against folklore, we prove that every , representable or not, has a universal normalization, a normal  which may be again representable or not.

§.§ Bibliography

Motivated by language theory and the representation theorem of Chomsky and Schützenberger, Melliès and Zeilberger <cit.> were the first to present the multicategorical splice-contour adjunction. We are indebted to their exposition, which we extend to the promonoidal and produoidal cases.  Our contribution is to show how  arise from an extended  splice-contour adjunction; unifying these two threads.

Street already noted that the endoprofunctors of a  had a duoidal structure <cit.>; Pastro and Street described a promonoidal structure on lenses <cit.> and Garner and López-Franco contributed a partial normalization procedure for duoidal categories <cit.>.
We build on top of this literature, putting it together, spelling out existence proofs, popularizing its produoidal counterpart and providing multiple new results and constructions that were previously missing (e.g. <Ref>).

This section takes its main ideas from joint work of this author with Matt Earnshaw and James Hefford <cit.>. Earnshaw and  <cit.> have described a syntactic congruence on formal languages of string diagrams using .

§ INTERLUDE: PRODUOIDAL NORMALIZATION

§.§ Normal Produoidal Categories

seem to contain too much structure: of course, we want to split things in two different ways, sequentially $(◁)$ and in parallel $(⊗)$; but that does not necessarily mean that we want to keep track of two different types of units, parallel $(I)$ and sequential $(N)$. The atomic components of our decomposition algebra should be the same, without having to care if they are atomic for sequential composition or atomic for parallel composition.

The monoidal spliced arrows we just introduced are a perfect example: if we simply want a hole in a string diagram, the type it may take depends on the wires we want to leave to each side (see <Ref>).
We would prefer to construct a new category – a Kleisli category on top of this one – where the bureaucracy of the units was already handled for us.

Multiple units complicate types.

§.§ The Normalization Monad

Fortunately, there exists an abstract procedure that, starting from any , constructs a new produoidal category where both units are identified. This procedure is known as normalization, and the resulting produoidal categories are called normal.

A normal produoidal category is a  where the unit interchanger $n \colon 𝕍(I;•) → 𝕍(𝖭;•)$ is an isomorphism.

form a category with produoidal functors between them, $\npDuo$. As a consequence, it is endowed with a fully faithful forgetful functor $𝓤 \colon \npDuo → \pDuo$.

Let $𝕍_{⊗,I,◁,N}$ be a  category. The profunctor

$$\NOR(𝕍)(•; •) = 𝕍(𝖭 ⊗ • ⊗ 𝖭; •)$$

forms a . Moreover, the Kleisli category of this  is a  with the following .

* $\NOR(𝕍)(X ⊗_𝖭 Y; Z) = 𝕍(𝖭 ⊗ X ⊗ 𝖭 ⊗ Y ⊗ 𝖭; Z)$;

* $\NOR(𝕍)(X ⊲_𝖭 Y; Z) = 𝕍((𝖭 ⊗ X ⊗ 𝖭) ⊲ (𝖭 ⊗ Y ⊗ 𝖭); Z)$; and

* $\NOR(𝕍)(I_𝖭;X) = \NOR(𝕍)(𝖭_𝖭;X) = 𝕍(𝖭;X)$.

Let us prove that $\NOR(𝕍)$ is a .
We now define the multiplication and unit for the , $\NOR(𝕍)$. They are constructed out of laxators of the produoidal category $𝕍$ and Yoneda isomorphisms; thus, they must be associative and unital by coherence. The unit is defined by (i) unitality of $𝕍$, (ii) the laxator of $𝕍$, and (iii) by definition of $\NOR(𝕍)$.

$$𝕍(X; Y) ≅ 𝕍(I ⊗ X ⊗ I; Y) → 𝕍(𝖭 ⊗ X ⊗ 𝖭; Y) ≅ \NOR(𝕍)(X; Y).$$

Multiplication is constructed as follows, using (i) the definition of $\NOR(𝕍)$, (ii) Yoneda reduction, (iii) the laxators of $𝕍$, and (iv) the definition of $\NOR(𝕍)$.

\begin{align*}
{\textstyle ∫}^{Y ∈ 𝕍} &\NOR(𝕍)(X; Y) × \NOR(𝕍)(Y; Z) =
{\textstyle ∫}^{Y ∈ 𝕍} 𝕍(𝖭 ⊗ X ⊗ 𝖭; Y) × 𝕍(𝖭 ⊗ Y ⊗ 𝖭; Z) \\
&≅ 𝕍(𝖭 ⊗ 𝖭 ⊗ X ⊗ 𝖭 ⊗ 𝖭; Y) → 𝕍(𝖭 ⊗ Y ⊗ 𝖭; Z) = \NOR(𝕍)(X; Z).
\end{align*}

Associativity and unitality follow from those of the .

The second part of this proof will show that $\NOR(𝕍)$ is indeed a : we will construct its associators, unitors and laxators from those of $𝕍$ and Yoneda isomorphisms. The right unitor is constructed as follows; the left unitor is constructed in a similar way: (i) by definition of $\NOR(𝕍)$, (ii) by associativity, (iii) by definition, (iv) by Yoneda reduction, (v) by definition, and (vi) by unitality.

\begin{align*}
& {\textstyle ∫}^{M ∈ \NOR(𝕍)} \NOR(𝕍)(𝖭; M) × \NOR(𝕍)(X ⊗_{𝖭} M; Y) &\quad
= & \\
& {\textstyle ∫}^{M ∈ \NOR(𝕍)} \NOR(𝕍)(𝖭; M) × 𝕍(𝖭 ⊗ X ⊗ 𝖭 ⊗ M ⊗ 𝖭; Y) &\quad
≅ & \\
& {\textstyle ∫}^{M ∈ \NOR(𝕍), P ∈ 𝕍} \NOR(𝕍)(𝖭; M) × 𝕍(𝖭 ⊗ M ⊗ 𝖭; P) ×  𝕍(𝖭 ⊗ X ⊗ P; Y) &\quad
= & \\
& {\textstyle ∫}^{M ∈ \NOR(𝕍), P ∈ 𝕍} \NOR(𝕍)(𝖭; M) × \NOR(𝕍)(M; P) × 𝕍(𝖭 ⊗ X ⊗ P; Y) &\quad
≅ & \\
& {\textstyle ∫}^{P ∈ 𝕍} \NOR(𝕍)(𝖭; P) × 𝕍(𝖭 ⊗ X ⊗ P; Y)  &\quad
= & \\
& {\textstyle ∫}^{P ∈ 𝕍} 𝕍(𝖭; P) × 𝕍(𝖭 ⊗ X ⊗ P; Y)  &\quad
≅ & \\
& 𝕍(𝖭 ⊗ X ⊗ 𝖭; Y).
\end{align*}

Let us now construct the associator in two steps: we will show that both sides of the following equation

\begin{align*}
& {\textstyle ∫}^{P ∈ \NOR(𝕍)} \NOR(𝕍)(Y ⊗_{𝖭} Z; P) × \NOR(𝕍)(X ⊗_{𝖭} P; A) \  ≅ \\
& {\textstyle ∫}^{M ∈ \NOR(𝕍)} \NOR(𝕍)(X ⊗_{𝖭} Y; M) × \NOR(𝕍)(M ⊗_{𝖭} Z; A)
\end{align*}

are isomorphic to $𝕍(𝖭 ⊗ X ⊗ 𝖭 ⊗ Y ⊗ 𝖭 ⊗ Z ⊗ 𝖭; A)$. The first side is isomorphic by (i) definition of $\NOR(𝕍)$, (ii) associativity of $𝕍$, (iii) definition of $\NOR(𝕍)$, (iv) Yoneda reduction, (v) definition of $\NOR(𝕍)$, and (vi) associativity. The second side is analogous.

\begin{align*}
& {\textstyle ∫}^{M ∈ \NOR(𝕍)} \NOR(𝕍)(Y ⊗_{𝖭} Z; M) × \NOR(𝕍)(X ⊗_{𝖭} M; A) &\quad
= & \\
& {\textstyle ∫}^{M ∈ \NOR(𝕍)} \NOR(𝕍)(Y ⊗_{𝖭} Z; M) × 𝕍(𝖭 ⊗ X ⊗ 𝖭 ⊗ M ⊗ 𝖭; A)  &\quad
≅ & \\
& {\textstyle ∫}^{M ∈ \NOR(𝕍), P ∈ 𝕍} \NOR(𝕍)(Y ⊗_{𝖭} Z; M) × 𝕍(𝖭 ⊗ M ⊗ 𝖭; P) × 𝕍(𝖭 ⊗ X ⊗ P; A) &\quad
= & \\
& {\textstyle ∫}^{M ∈ \NOR(𝕍), P ∈ 𝕍} \NOR(𝕍)(Y ⊗_{𝖭} Z; M) × \NOR(𝕍)(M; P) × 𝕍(𝖭 ⊗ X ⊗ P; A) &\quad
≅ & \\
& {\textstyle ∫}^{P ∈ 𝕍} \NOR(𝕍)(Y ⊗_{𝖭} Z; P) × 𝕍(𝖭 ⊗ X ⊗ P; A) ×  &\quad
= & \\
& {\textstyle ∫}^{P ∈ 𝕍} 𝕍(𝖭 ⊗ Y ⊗ 𝖭 ⊗ Z ⊗ 𝖭; P) × 𝕍(𝖭 ⊗ X ⊗ P; A) &\quad
≅ & \\
& 𝕍(𝖭 ⊗ X ⊗ 𝖭 ⊗ Y ⊗ 𝖭 ⊗ Z ⊗ 𝖭; A).
\end{align*}

Finally, let us construct the four interchangers that define the . Three of them are immediate: they are either identities or unitors: $\NOR(𝕍)(I_{𝖭},A) ≅ \NOR(𝕍)(I_{𝖭} ⊲ I_{𝖭}; A)$ is the first, $\NOR(𝕍)(𝖭 ⊗ 𝖭; A) ≅ \NOR(𝕍)(𝖭; A)$ is the second, and $\NOR(𝕍)(I_{𝖭};A) ≅ \NOR(𝕍)(𝖭_{𝖭};A)$ is the last one. We note here that this  is natural because of these isomorphisms. Thus, we only need to construct the first interchanger morphism of a ,

\NOR(𝕍)((X₁ ⊲ Y₁) ⊗ (X₂ ⊲ Y₂); A) \longrightarrow
\NOR(𝕍)((X₁ ⊗ X₂) ◁ (Y₁ ⊗ Y₂); A),

which is defined by the following reasoning. Here, we abbreviate $𝖭 ⊗ X ⊗ 𝖭$ by $X^{⊗𝖭}$, and we apply (i) the definition of the tensors of $\NOR(𝕍)$, (ii) the interchanger of $𝕍$, (iii) unitality in $𝕍$, and (iv) the definition of tensors of $\NOR(𝕍)$.

\begin{align*}
& \NOR(𝕍)((X₁ ⊲_{𝖭} Y₁) ⊗_{𝖭} (X₂ ⊲_{𝖭} Y₂); A) && = \\
& 𝕍(𝖭 ⊗ (X_1^{⊗𝖭} ⊲ Y_1^{⊗𝖭}) ⊗ 𝖭 ⊗ (X_2^{⊗𝖭} ⊲ Y_2^{⊗𝖭}) ⊗ 𝖭; A) & & \to  \\
& 𝕍((𝖭 ⊗ X_1^{⊗𝖭} ⊗ 𝖭 ⊗ Y_1^{⊗𝖭} ⊗ 𝖭) ⊲ (𝖭 ⊗ X_2^{⊗𝖭} ⊗ 𝖭 ⊗ Y_2^{⊗𝖭} ⊗ 𝖭); A) & & \to  \\
& 𝕍((𝖭 ⊗ X_1 ⊗ 𝖭 ⊗ Y_1 ⊗ 𝖭)^{⊗𝖭} ⊲ (𝖭 ⊗ X_2 ⊗ 𝖭 ⊗ Y_2 ⊗ 𝖭)^{⊗𝖭}; A) & & \to  \\
& \NOR(𝕍)((X_1 ⊗_{𝖭} Y_1) ⊲_{𝖭} (X_2 ⊗_{𝖭} Y_2); A).
\end{align*}

The structure equations of the laxators follow from those of the base category $𝕍$. This finishes the construction of a  on the Kleisli category of the .

Normalization extends to an idempotent monad.

The first part of the proof will show that $\NOR(𝕍)$ is the free  over $𝕍$ by constructing the a monad structure on top of the functor $\NOR ፡ \npDuo → \npDuo$. Let us construct the unit and the multiplication of the monad.
The unit $\eta_{𝕍} : 𝕍 → \NOR(𝕍)$ is defined as the identity-on-objects functor associated to the ; it and acts on morphisms by the unit of the promonad. Let us show that this is a  by constructing the following components; all of them use the map $I → 𝖭$ from the base ,

* $η_{⊗} ፡ 𝕍(X ⊗ Y; A) → 𝕍(I ⊗ X ⊗ I ⊗ Y ⊗ I; A) → 𝕍(𝖭 ⊗ X ⊗ 𝖭 ⊗ Y ⊗ 𝖭; A)$;

* $η_{I} : 𝕍(I;A) → 𝕍(𝖭;A)$;

* $η_{⊲} : 𝕍(X ⊲ Y; A) → 𝕍((I ⊗ X ⊗ I) ⊲ (I ⊗ Y ⊗ I); A) → 𝕍((𝖭 ⊗ X ⊗ 𝖭) ⊲ (𝖭 ⊗ Y ⊗ 𝖭); A)$;

* $η_{𝖭} : 𝕍(𝖭; A) → 𝕍(𝖭;A)$ is simply an identity.

these preserve laxators and coherence maps since they are constructed only from laxators and coherence maps.

Let us construct now the multiplication of the monad, $μ_{𝕍} : \NOR(\NOR(𝕍)) → \NOR(𝕍)$, and show that it is an isomorphism, making it an idempotent monad. The underlying functor is identity on objects, and it acts on morphisms by
the normality of the already normalized ,

$$\NOR(\NOR(𝕍))(X;Y) = \NOR(𝕍)(𝖭 ⊗_{𝖭} X ⊗_{𝖭} 𝖭; Y) ≅ \NOR(𝕍)(X;Y).$$

The following components make this functor a , they are constructed again from the normality of the already normalized :

* $\mu_{⊗} : \NOR(\NOR(𝕍))(X ⊗_{𝖭𝖭} Y; A) = \NOR(𝕍)(𝖭 ⊗_𝖭 X ⊗_𝖭 𝖭 ⊗_𝖭 Y ⊗_𝖭 𝖭; A) ≅ \NOR(𝕍)(X ⊗_N Y;A)$;

* $\mu_{⊲} : \NOR(\NOR(𝕍))(X ⊲_{𝖭𝖭} Y; A) = \NOR(𝕍)((𝖭 ⊗_𝖭 X ⊗_𝖭 𝖭) ⊲_𝖭 (𝖭 ⊗_𝖭 Y ⊗_𝖭 𝖭); A) ≅ \NOR(𝕍)(X ⊲_𝖭 Y; A)$;

* $\mu_{I} : \NOR(\NOR(𝕍))(𝖭;A) = \NOR(𝕍)(𝖭;A)$;

* $\mu_{𝖭} : \NOR(\NOR(𝕍))(𝖭;A) = \NOR(𝕍)(𝖭;A)$,

Finally we verify the monad laws. $η_{𝓝𝕍} ⨾ \mu_{𝕍}$ is an identity-on-objects; on morphisms, it applies left and right unitors followed by their inverses; as a consequence, its underlying functor is the identity.
The components of the natural transformations are also identities, since the interchanger $I → 𝖭$ is an identity for the normalized  $\NOR(𝕍)$; they are otherwise composed of unitors followed by their inverses. The last step is to check the associativity of the monad, $\mu_{\NOR(𝕍)} ⨾ \mu_𝕍$ and $\NOR(\mu_{𝕍}) ⨾ \mu_𝕍$; this is simply the identity on objects, so we simply apply left and right unitors twice on morphisms and their components.

A  $𝕍$ has exactly one algebra structure for the normalization monad when it is normal, and none otherwise.

Let $(F, F_{⊗}, F_I, F_{𝖭}, F_𝖭) ፡ \NOR(𝕍) → 𝕍$ be an algebra. This means that the following commutative diagrams with the unit and multiplication of the normalization monad must commute.

𝕍 [r, "η"] [rd, "id"', no head]     (𝕍) [d, "F"]          ((𝕍)) [r, "μ"] [d, "(F)"']     (𝕍) [d, "F"]

𝕍        (𝕍) [r, "F"']     𝕍

Now, consider how the interchanger $ψ_0 ፡ 𝕍(I; •) → 𝕍(𝖭; •)$ is transported by these maps.

𝕍(𝖭; •) [rd, "F_I"] [d, "id"]

𝕍(I; •) [ru, "η_I"] [d, "ψ_0"'] [rr, "id"', bend right]
𝕍(𝖭; •) [rd, "F_N"']
𝕍(I; •) [d, "ψ_0"]

𝕍(𝖭; •) [ru, "id"'] [rr, "id"', bend right]
𝕍(𝖭; •)

We conclude that $η_I = ψ_0$, but also that $F_𝖭 = \mathrm{id}$. As a consequence, $ψ_0$ is invertible and $F_I$ must be its inverse. We have shown that any  that is an algebra for the normalization monad must be normal.

We will now show that this already determines all of the functor $F$.  We know that $η_{⊗}, η_{◁}, η$ are isomorphisms because they are constructed from the unitors, associators, and the laxator $ψ_0$, which is an isomorphism in this case. This determines that $F_{⊗}, F_{⊲}, F$ must be their inverses. By construction, these satisfy all structure equations.

Normalization determines an adjunction between  and ,

$$\NOR ፡ \ProDuo \rightleftharpoons \npDuo \colon \mathsf{Forget}.$$

That is, $\NOR(𝕍)$ is the free  over $𝕍$.

We know that the algebras for the normalization monad are exactly the  (<Ref>). We also know that the normalization monad is idempotent (<Ref>).
This implies that the forgetful functor from its category of algebras is fully faithful, and thus, the algebra morphisms are exactly the produoidal functors. As a consequence, the canonical adjunction to the category of algebras of the monad is exactly an adjunction to the category of .

Garner and López Franco <cit.> introduced a partial normalization procedure for duoidal categories.
We contribute a general normalization procedure for  and we characterize it universally.
Produoidal normalization behaves slightly better than duoidal normalization: it always succeeds, and we prove that it forms an idempotent monad (<Ref>).
The technical reason for this improvement is that the original duoidal normalization required the existence of certain coequalizers in $𝕍$; produoidal normalization uses coequalizers in $\Set$.

In the previous <Ref>, we constructed the  of , which distinguishes between morphisms and morphisms with a hole in the monoidal unit.
This is because the latter hole splits the morphism in two parts.
Normalization equates both; it sews these two parts.
In <Ref>, we explicitly construct monoidal contexts, the normalization of . Before that, let us also introduce the symmetric version of normalization.

§.§ Symmetric Normalization

Normalization is a generic procedure that applies to any , it does not matter if the parallel join $(⊗)$ is symmetric or not. However, when $⊗$ happens to be symmetric, we can also apply a more specialized normalization procedure: symmetric normalization.

A symmetric produoidal category is a  $𝕍_{◁,N,⊗,I}$ endowed with a natural isomorphism
$σ ፡ 𝕍(X ⊗ Y;Z) ≅ 𝕍(Y ⊗ X; Z)$ satisfying the symmetry and hexagon equations.

Let $𝕍$ be a  category. The profunctor

$$\sNOR(𝕍)(• ; •) =𝕍(N ⊗ •; •)$$

forms a . Moreover, the Kleisli category of this  is a normal  category with the following .

* $\sNOR(𝕍)(X ⊗_N Y; Z) = 𝕍(N ⊗ X ⊗ Y; Z)$;

* $\sNOR(𝕍)(X ⊲_𝖭 Y; Z) = 𝕍((N ⊗ X) ◁ (N ⊗ Y); Z)$; and

* $\sNOR(𝕍)(I_𝖭; X) =\sNOR(𝕍)(𝖭_𝖭; X) = 𝕍(𝖭; X)$.

Normalization determines an adjunction between  and normal  categories,

$$\sNOR ፡ \symProDuo \rightleftharpoons \nSymProduo \colon 𝓤.$$

That is, $\sNOR(𝕍)$ is the free normal  category over $𝕍$.

§.§ Bibliography

Garner and López-Franco contributed a partial normalization procedure for duoidal categories <cit.>, all of the credit for this elegant idea goes there.

We contribute its produoidal counterpart. The reader could think that this is an automatic process: extending an argument by Day <cit.>,  could be understood as closed  in some sense. However, we show that there are some technical differences that make this case important: in the work of Garner and López-Franco, not every  has a normalization, and this prevents us from constructing a monad. We prove that produoidal normalization is always possible and defines an idempotent monad.

§ MONOIDAL LENSES

– the name we give to  <cit.> – formalize the notion of an incomplete morphism in a monoidal category. The category of  will have a rich algebraic structure: we shall be able to still compose contexts sequentially and in parallel and, at the same time, we shall be able to fill a context using another monoidal context. Perhaps surprisingly, then, the category of  is not even monoidal.

We justify this apparent contradiction in terms of profunctorial structure: the category is not monoidal, but it does have two  structures that precisely represent sequential and parallel composition. These structures form a .
In fact, we show it to be the normalization of the  category of . This section constructs explicitly this  of .

§.§ The Category of Monoidal Lenses

A  – an element of type $\pbiobj{X}{Y} → \pbiobj{A}{B}$ – represents a process from $A$ to $B$ with a hole admitting a process from $X$ to $Y$. In this sense,  are similar to . The difference with  is that  allow for communication to happen to the left and to the right of this hole.

Let $(ℂ,⊗,I)$ be a . Monoidal lenses are the elements of the

$$\mLens\left({\biobj{X}{Y}}; \biobj{A}{B}\right) = ∫^{M_1,M_2} ℂ(A;M_1⊗X⊗M_2) × ℂ(M_1⊗Y⊗M_2;B).$$

In other words, a monoidal lens from $A$ to $B$, with a hole from $X$ to $Y$, is an equivalence class consisting of a pair of objects $M, N ∈ \obj{ℂ}$ and a pair of morphisms $f ∈ ℂ(A; M⊗X⊗N)$  and $g ∈ ℂ(M⊗Y⊗N;B)$, quotiented by dinaturality of $M$ and $N$.

Let $(ℂ,⊗,I)$ be a .
Its  of monoidal lenses, $\mLens(ℂ)$, has objects formed by pairs, $\mLens(ℂ)_{obj} = (ℂ^{op} × ℂ)_{obj}$, and is defined by the following .

* Morphisms are diagrams with a single typed hole.
$$\mLens{ℂ} \left( \biobj{X}{Y} ; \biobj{A}{B}\right) =  ∫^{M_1,M_2} ℂ(A;M_1⊗X⊗M_2) × ℂ(M_1⊗Y⊗M_2;B),$$

*  are diagrams with a pair of sequential holes.

$$\begin{aligned} \mLens{ℂ}(\biobj{X}{Y} ⊲ \biobj{X'}{Y'}; \biobj{A}{B};) =  ∫^{M_1,M_2}  &ℂ(A;M_1⊗X⊗M_2) × ℂ(M_1⊗Y⊗M_2;\\& M_3 ⊗X'⊗M_4) × ℂ(M_3⊗Y'⊗M_4; B);\end{aligned}$$

*  are diagrams with a pair of parallel holes.

\mLens{(ℂ)}(\biobj{X}{Y} ⊗ \biobj{X'}{Y'}; \biobj{A}{B}) = ∫^{M₁,M₂,M₃} &ℂ(A; M₁ ⊗ X ⊗ M₂ ⊗ X' ⊗ M₃) × \\&  ℂ(M₁  ⊗ Y ⊗ M₂ ⊗ Y' ⊗ M₃; B)\end{aligned}$$

* Units are complete diagrams with no holes,
$\mLens{(ℂ)}(𝖭;\biobj{X}{Y}) = ℂ(X;Y).$

Reading the profunctorial notation can be unenlightening.
We provide the incomplete string diagrams for these profunctors in <Ref> <cit.>.

Monoidal lenses.

The category of  forms a normal  with its units, sequential and parallel joins.
are the free normalization of the cofree  over a category.
In other words,  are the normalization of ,

$$\mLens{(ℂ)} ≅ \NOR(\mSplice{ℂ}).$$

The core of this result is in <Ref>, which says that the normalization procedure yields the free normalization over a . It is only left to check that this  of  that we have explicitly constructed in this section is precisely the normalization of the linkProduoidalSpliceproduoidal category of spliced arrows. We do so for morphisms, the rest of the proof is similar; the proof shows that $\mSplice{ℂ} \left(  𝖭 ⊗ \biobj{X}{Y} ⊗ 𝖭 ; {\biobj{A}{B}} \right)$, the normalization of spliced monoidal arrows, is isomorphic to monoidal lenses, $\mLens(ℂ)\left( {\biobj{A}{B}};{\biobj{X}{Y}} \right)$. We employ the Yoneda lemma on both $V$ and $V'$.

\begin{align*}
& ∫^{U, V, U', V' ∈ ℂ}
ℂ(A; U ⊗ X ⊗ U') ×
ℂ(V ⊗ Y ⊗ V'; B) ×
ℂ\left(U ; V \right) ×
ℂ\left(U' ; V' \right)
& ≅ \\
& ∫^{U,U' ∈ ℂ}
ℂ\left( A ; U ⊗ X ⊗ U'\right) ×
ℂ(U ⊗ Y ⊗ U' ; B)
\end{align*}

The rest of the profunctors follow a similar reasoning.

§.§ Symmetric Monoidal Lenses

A  of type $\smLens{(ℂ)}(\biobj{X}{Y}; \biobj{A}{B})$ represents a process in a  with a hole admitting a process from $X$ to $Y$.

are , but we stop caring where the hole is.
Again, the category of  has a rich algebraic structure; and again, most of this structure exists only virtually in terms of profunctors. In this case, though, the monoidal tensor does indeed exist: contrary to ,  form also a .
This is perhaps why applications of  have grown popular in recent years <cit.>, with applications in decision theory <cit.>, supervised learning <cit.> and most notably in functional data accessing <cit.>.
The  structure of optics was ignored, even when, after now identifying for the first time its relation to the monoidal structure of optics, we argue that it could be potentially useful in these applications: e.g. in multi-stage decision problems, or in multi-stage data accessors.

This section explicitly constructs the normal  of symmetric monoidal lenses.
We describe it for the first time by a universal property: it is the free symmetric normalization of the cofree .

Let $(ℂ,⊗,I)$ be a symmetric .
Symmetric monoidal lenses are the elements of the profunctor

$$\smLens{ℂ}\left(\biobj{X}{Y}; \biobj{A}{B} \right) = ∫^M ℂ(A ; M ⊗ X) × ℂ(M ⊗ Y ; B).$$

In other words, a symmetric monoidal lens from $A$ to $B$, with a hole from $X$ to $Y$, is an equivalence class consisting of a pair of objects $M ∈ ℂ_{obj}$ and a pair of morphisms $f ∈ ℂ(A; M ⊗ X)$  and $g ∈ ℂ(M ⊗ Y;B)$, quotiented by  of $M$.

Let $(ℂ,⊗,I)$ be a .
Its  of symmetric monoidal lenses, $\smLens{(ℂ)}$, has objects formed by pairs, $\smLens{(ℂ)}_{obj} = (ℂ^{op} × ℂ)_{obj}$, and is defined by the following .

* Morphisms are diagrams with a single typed hole.

$$\smLens{(ℂ)} \left(\biobj{X}{Y} ; \biobj{A}{B} \right) =  ∫^{M} ℂ(A;M ⊗X) × ℂ(M⊗Y;B),$$

*  are diagrams with a pair of sequential holes.

\smLens(ℂ)( \biobj{X}{Y} ⊲ \biobj{X'}{Y'} ; \biobj{A}{B}) =  ∫^{M_1,M_2}  &ℂ(A;M_1⊗X) × ℂ(M_1⊗Y;\\& M_2 ⊗X') × ℂ(M_2 ⊗ Y'; B);
\end{aligned}$$

*  are diagrams with a hole encompassing parallel wires.

\smLens(ℂ)(\biobj{X}{Y} ⊗ \biobj{X'}{Y'}; \biobj{A}{B}) = ∫^{M} &ℂ(A; M ⊗ X ⊗ X') ×  ℂ(M ⊗ Y ⊗ Y'; B).
\end{aligned}$$

* Units are complete diagrams with no holes,
$\smLens(ℂ)(𝖭; \biobj{A}{B}) = ℂ(A;B).$

Reading the profunctorial notation can be unenlightening.
We provide the incomplete string diagrams for these profunctors in <Ref> <cit.>.
The only substantial difference with  is that we do not need to keep track of where the hole is placed.

Symmetric monoidal lenses.

The term “” has usually been reserved for the morphisms of this category; in the literature, the sequential splits  – the lenses with multiple holes – get a name from their distinctive shape: these are combs or quantum combs <cit.>.

§.§ Towards Message Theories

Lenses, or combs, can be interpreted as incomplete morphisms, but also as morphisms that send and receive resources. The next chapter will exploit this intuition.

We will write $A^{∘} = \pbiobj{A}{I}$ and $B^{•} = \pbiobj{I}{B}$ for the objects of the symmetric  of lenses that have a monoidal unit as one of its objects. Thanks to $A^{∘} ⊗ B^{•} = \pbiobj{A}{B}$, these are enough to express all objects.

Let $(ℂ,⊗,I)$ be a symmetric . There exist monoidal functors

$$(\Send{}) ፡ ℂ → \smLens(ℂ), \quad\mbox{ and }\quad (\Get{}) \colon ℂ^{op} → \smLens(ℂ).$$

Moreover, they satisfy the following properties definitionally:
$ℂ( \Get{A} ⊲ \Get{B} ; •) ≅ ℂ(\Get{A} ⊗ \Get{B}; •)$;
$\Send{(A ⊗ B)} = \Send{A} ⊗ \Send{B}$;
$ℂ(\Send{A} ⊲ \Send{B}; •) ≅ ℂ(\Send{A} ⊗ \Send{B}; •)$;
$\Get{(A ⊗ B)} = \Get{A} ⊗ \Get{B}$; and
$ℂ(\Send{A} ⊲ \Get{B}; •) ≅ ℂ(\Send{A} ⊗ \Get{B}; •)$.

We define $\Send{f} = (f ⨾ □ ⨾ \id_I)$ and $\Get{g} = (\id_I ⨾ □ ⨾ g)$, and then check that compositions and tensoring of morphisms are compatible with composition and tensoring of , this is straightforward.
Moreover, we can see that, by definition,

\begin{align*}
& \Send{(A ⊗ B)} = \left(\biobj{A ⊗ B}{I}\right) = \left(\biobj{A}{I}\right) ⊗ \left(\biobj{B}{I}\right) = \Send{A} ⊗ \Send{B}, \quad\mbox{ and } \\
&\Get{(A ⊗ B)} = \left(\biobj{I}{A ⊗ B}\right) = \left(\biobj{I}{A}\right) ⊗ \left(\biobj{I}{B}\right) = \Get{A} ⊗ \Get{B}.
\end{align*}

This proof appears with a different language in the work of Riley <cit.>. In fact, there, the combined identity-on-objects functor $({∘} × {•}) ፡ ℂ × ℂ^{op} → \smLens(ℂ)$ is shown to be monoidal.

Let us give a first example of how to employ combs for the description of concurrent protocols.
Broadbent and Karvonen <cit.> propose a formalization of the one-time pad encryption protocol in a  endowed with a Hopf algebra with an integral.

Theory of a Hopf algebra with an integral.

A Hopf algebra with an integral, $(X,\iconbcm,\iconbcu,\iconwm,\iconwu,i,d)$, is a commutative bialgebra endowed with an antipode map $i ፡ X → X$, representing inversion; and endowed with an integral map, $d ፡ I → X$, representing a non-determined value, or pure noise. These must satisfy the equations in <Ref>.

The one-time pad is a mathematically secure encryption technique. It works as follows: (i) the two parties communicating – say,  and  – start by preparing some random bits and sharing them; (ii) when the message is ready,  applies bitwise XOR with the random bits to encrypt the message, and then broadcasts the encrypted message – a potential attacker, , will receive this encrypted message; (iii) finally,  receives the encrypted message and applies again bitwise XOR with the random bits to decrypt the message (<Ref>).

Description of the one-time pad.

The one-time pad is secure, meaning that it is equal to the process that sends a message from  to  and outputs random noise through the attacker's channel.

We repeat the proof from Broadbent and Karvonen <cit.>.
We employ string diagrams of , in <Ref>, to show that the morphism is equal to an identity tensored by the integral of the Hopf algebra.

Correctness of the one-time pad.

The interesting part comes when we want to split the morphism into its different constituents: there should be a stage where the three actors play;  does not control the fact that the encrypted message will be broadcast; , the attacker, can only attack at the end;  will need to keep a bit in memory. These considerations are part of the problem statement the one-time pad is solving. It is easy to come up with a morphism that connects an input to an output: the problem the one-time pad is solving is to do so on a stage that has been preset.

The components of the one time pad are not simply morphisms of a  (<Ref>). They must be understood as . After this section, we can declare that a possible typing for these components is the following:

* $\Alice ፡ 𝖭 → \pbiobj{X ⊗ X}{X}$;

* $\Bob ፡ X^{•} ⊲ X^{∘} → \pbiobj{I}{X}$;

* $\Eve ፡ 𝖭 → \pbiobj{X}{X}$;

* $\mathsf{Stage} ፡ X^{∘} ⊲ X^{•} ⊲ X^{•} ⊲ X^{∘} ⊲ X^{•} ⊲ X^{•} ⊲ X^{∘} ⊲ X^{∘} → \pbiobj{X}{X ⊗ X}$;

Components of the one-time pad.

Still, at this stage it is not easy to talk about message passing with this syntax. It is true that the new produoidal types can track all the exchanges that happen along a boundary; but these types are tedious – see, for instance, the long type of $\mathsf{Stage}$ – and it is not clear how to compose them. What we are missing is a combinatorial description of the different ways we can combine elements of this produoidal algebra.

This is what the next chapter will solve: we will propose a combinatorial algebra of message passing and show that lenses, the normalized cofree produoidal algebra over a  have a second universal property – they also constitute the free .

§.§ Bibliography

Lenses <cit.> are a notion of bidirectional transformation that can be cast in arbitrary monoidal categories.
The first mention of monoidal lenses separate from their classical database counterparts <cit.> is due to Pastro and Street <cit.>, who identify them as an example of a . However, it was with a different monoidal structure <cit.> that they became popular in recent years, spawning applications not only in bidirectional transformations <cit.> but also in functional programming <cit.>, open games <cit.>, polynomial functors <cit.> and quantum combs <cit.>.
Relating this monoidal category of lenses with the previous  of lenses was an open problem; and the  structure was mostly ignored in applications.
We solve this problem, proving that lenses are a universal normal  category (the ), which endows them with a novel algebra and a novel universal property.
This also extends work on the relation between incomplete diagrams, comb-shaped diagrams, and lenses <cit.>.

Lenses themselves have been applied to protocol specification <cit.>.
Spivak <cit.> also discusses the  of wiring diagrams, later used for incomplete diagrams <cit.> and related to lenses <cit.>; we conjecture that this  of wiring diagrams is precisely the  of lenses, once we stop tracking dependencies explicitly.

Each physical  induces a  given by its physical lax tensor (<Ref>).
The  of wiring diagrams <cit.> of  is the  induced by the  of .

The  we use can be seen as  with an extra coherence property. In this sense, we contribute the missing algebraic structure of the universal multicategory of wiring diagrams relative to a monoidal category.

CHAPTER: MONOIDAL MESSAGE PASSING

§ MONOIDAL MESSAGE PASSING

This chapter develops message passing in  following the theory of context we just constructed. We have already defined what incomplete morphisms in  are: we will now study the structure of all their possible compositions. This includes not only the obvious operations of composition but any possible wiring of a diagram that could combine them while respecting the acyclicity of string diagrams.

Studying seriously the combinatorial structure of  composition arrives at the same conclusion as axiomatizing a naive theory of message passing: . Indeed, we prove that the polarized shufflings that describe  composition have as algebras precisely the .

<Ref> introduces our minimalistic theory of message passing, with axioms that should hopefully be  acceptable to any reader. <Ref> starts developing the categorical semantics for , based on  (a variant of ); it then shows that shufflings from the free . <Ref> provides the second ingredient for this categorical semantics: polarization. We then combine both ingredients in <Ref>:  form the combinatorial structure that combines incomplete string diagrams;  are precisely the algebras of  of . This chapter ends with an adjunction between  and , which ensures that we can construct a free  on top of any .

§ MESSAGE THEORIES

§.§ Message Theories

Message passing requires the interplay of at least two mathematical structures: the ability to interleave events in time and the ability to connect a sender and a receiver.
Let us propose a minimally axiomatized algebra of interleaving and sending/receiving: interleaving will correspond to a normal duoidal algebra, and sending/receiving will correspond to polarization.

A message theory $𝕄$ consists of a set of types, $𝕄_{obj}$ with extra structure: a send/receive session type is a polarized list of types; for each session type, we have a collection of sessions with that type,

$$𝕄( X₁^{‽₁} , … , Xₙ^{‽ₙ} ), \mbox{ for each } X₁, …, Xₙ ∈ 𝕄_{obj}, \mbox{ and each polarization } ‽ᵢ ∈ \{{∘},{•}\}.$$

A  must contain operations for (i) binary shuffling, (ii) and nullary shuffling, (iii) linking a sent message to immediately receive it, and (iv) spawning a channel that receives a message and sends it immediately.

* $\SHF_{σ} ፡ 𝕄(Γ) × 𝕄(Δ) → 𝕄({σ}(Γ,Δ))$, shuffling two processes;

* $\NOP ፡ 𝕄()$, a no-operation, doing nothing;

* $\LNK_x^{Γ;Δ} ፡ 𝕄(Γ, X^{•}, X^{∘}, Δ) → 𝕄(Γ, Δ)$, linking send to receive;

* $\SPW_x^{Γ;Δ} ፡ 𝕄(Γ, Δ) → 𝕄(Γ, X^{∘}, X^{•}, Δ)$, a receive to send channel.

may be better understood in the notation of a logic, as in <Ref>. Types form a free polarized monoid; each term describes a possible communication protocol.

Γ     Δ

Γ, X^•, X^∘, Δ
Γ, Δ

Γ, Δ
Γ, X^∘, X^•, Δ

Type-theoretic presentation of a message theory.

A message theory must satisfy the following axioms: (i) shuffles compose as in their symmetric , where we write $(σ ⨾₁ τ)$ to be the same by associativity as $(τ' ⨾₂ σ')$, we write $(\ast)$ for the trivial shuffle, and we write $\tilde{σ}$ for the symmetric counterpart of $σ$; (ii) linking is natural with respect to the shuffles; (iii) spawning is natural with respect to the shuffles; (iv) linking is dual to spawning; and (v) independent linkings and spawnings commute.

(1a) $\SHF_{τ}(\SHF_{σ}(m₁m₂),m₃) = \SHF_{σ'}(m₁,\SHF_{τ'}(m₂,m₃))$;

(1b) $\SHF_{\ast}(m, \NOP) = m$;

(1c) $\SHF_{σ}(m₁,m₂) = \SHF_{\tilde{σ}}(m₂,m₁)$;

(2a) $\SHF_{σ,τ}(\LNK_x^{Γ₁,Γ₂}(m₁), m₂) = \LNK_x^{Γ₁,Δ₁;Γ₂,Δ₂}(\SHF_{σ,x,τ}(m₁,m₂))$;

(2b) $\SHF_{σ,τ}(m₁, \LNK_x^{Δ₁,Δ₂}(m₂)) = \LNK_x^{Γ₁,Δ₁;Γ₂,Δ₂}(\SHF_{σ,x,τ}(m₁,m₂))$;

(3a) $\SHF_{σ,τ}(\SPW_x^{Γ₁,Γ₂}(m₁), m₂) = \SPW_x^{Γ₁,Δ₁;Γ₂,Δ₂}(\SHF_{σ,τ}(m₁,m₂))$;

(3b) $\SHF_{σ,τ}(m₁, \SPW_x^{Δ₁,Δ₂}(m₂)) = \SPW_x^{Γ₁,Δ₁;Γ₂,Δ₂}(\SHF_{σ,τ}(m₁,m₂))$;

(4a) $\LNK_{x}^{Γ,X^{∘};Δ}(\SPW_x^{Γ;X^{∘},Δ}(m)) = m$;

(4b) $\LNK_{x}^{Γ;X^{•},Δ}(\SPW_x^{Γ,X^{•};Δ}(m)) = m$;

(5a) $\LNK_{x}^{Γ₁;Γ₂YΓ₃}(\SPW_y^{Γ₁XΓ₂;Γ₃}(m)) = \SPW_y^{Γ₁Γ₂;Γ₃}(\LNK_x^{Γ₁;Γ₂Γ₃}(m))$;

(5b) $\LNK_{y}^{Γ₁XΓ₂;Γ₃}(\SPW_x^{Γ₁;Γ₂YΓ₃}(m)) = \SPW_x^{Γ₁;Γ₂Γ₃}(\LNK_y^{Γ₁XΓ₂;Γ₃}(m))$;

(5c) $\SPW_{x}^{Γ₁;Γ₂YΓ₃}(\SPW_y^{Γ₁Γ₂;Γ₃}(m)) = \SPW_y^{Γ₁XΓ₂;Γ₃}(\SPW_x^{Γ₁;Γ₂Γ₃}(m))$;

(5d) $\LNK_{x}^{Γ₁;Γ₂Γ₃}(\LNK_y^{Γ₁XΓ₂;Γ₃}(m)) = \LNK_y^{Γ₁Γ₂;Γ₃}(\LNK_x^{Γ₁;Γ₂YΓ₃}(m))$.

These axioms are again better understood in logic notation, as equations between derivations, see <Ref>.

Axioms of a message theory.

A message functor $F ፡ 𝕄 → ℕ$ between two , $𝕄$ and $ℕ$, is a function on objects $F_{obj} ፡ 𝕄_{obj} → ℕ_{obj}$ that extends to a family of functions on session sets,

$$F ፡ 𝕄(X_1^{‽},…,X_n^{‽}) → ℕ(FX_1^{‽},…,FX_n^{‽}).$$

This function must (i) preserve shuffling, $F(\SHF_{σ}(f,g)) = \SHF_{σ}(Ff,Fg)$; (ii) preserve spawning, $F(\SPW_x) =\SPW_{Fx}$; (iii) connecting, $F(\COM_x(f)) = \COM_x(Ff)$; and (iv) the no-operation, $F(\NOP) = \NOP$.  form a category $\mathbf{Msg}$ with message functors between them.

§.§ Properties of a Message Theory

Our goal is to prove a coherence theorem for . Building up to this result, let us reason with  to understand the basic properties that can be derived from the axioms.

have a derived operation for each shuffling; moreover, these operations compose as in the  of shufflings.

$$\mathsf{shuf}_{σ}^{Γ₁,…,Γₙ} ፡ 𝕄(Γ₁) × \dots × 𝕄(Γₙ) → 𝕄([Γ₁,…,Γₙ]_{σ})$$

We have defined an operation for binary and nullary shufflings, and we have defined them to compose exactly as shufflings do. Because shufflings form a , each n-ary shuffling can be recovered uniquely from the binary and nullary shufflings.

A session can always send later and receive sooner, but it cannot send sooner nor receive later. Formally, there exist derived operations

\begin{align*}
\mathsf{wait}_X^{Γ,Δ,Ψ} ፡ 𝕄(Γ,X^{•},Δ,Ψ) → 𝕄(Γ, Δ, X^{•},Ψ), \\
\mathsf{rush}_X^{Γ,Δ,Ψ} ፡ 𝕄(Γ, Δ, X^{∘},Ψ) → 𝕄(Γ,X^{∘},Δ,Ψ).
\end{align*}

We can construct the derivation trees of both operations. They both spawn a new channel, shuffle its ends to the origin and target position, and they connect the channel.

Γ, X^•, Δ, Ψ
*[Right=(spw)]XX^∘, X^•
Γ, X^•, X^∘, Δ, X^•, Ψ
Γ, Δ, X^•, Ψ

Γ, Δ, X^∘, Ψ
*[Right=(spw)]XX^∘, X^•
Γ, X^∘, Δ, X^∘, X^•, Ψ
Γ,X^∘, Δ,  Ψ

Derivation of $\mathsf{wait}$ and $\mathsf{rush}$.

The explicit construction is in <Ref>. Note how, thanks to polarization, it is not possible to use the same technique to send sooner nor receive later. In fact, we can reason by contradiction that sending sooner, $𝕄(Γ,Δ,X^{•},Ψ) → 𝕄(Γ, X^{•}, Δ, Ψ)$, is impossible: the only possible operations we can apply in an arbitrary message theory to an arbitrary session are shufflings with a spawned channel and connections; we require at least a connection to eliminate the $X^{•}$, but because the $X^{∘}$ must come from shuffling a spawned channel, the corresponding $X^{•}$ must be placed strictly after it.

In particular, we can always swap the order of objects with the same polarity,

\begin{align*}
\mathsf{swap}^{Γ;X;Y;Δ}_{∘} ፡ 𝕄(Γ,X^{∘},Y^{∘},Δ) → 𝕄(Γ,Y^{∘},X^{∘},Δ), \\
\mathsf{swap}^{Γ;X;Y;Δ}_{•} ፡ 𝕄(Γ,X^{•},Y^{•},Δ) → 𝕄(Γ,Y^{•},X^{•},Δ).
\end{align*}

These are self-inverses, forming not only braidings but symmetries in the underlying  of positively or negatively polarized objects.

Swaps are constructed from rushing and waiting (<Ref>); explicitly,

$$\mathsf{swap}^{Γ;X;Y;Δ}_{∘} = \mathsf{rush}_Y^{Γ,X^{∘},Ψ},\quad\mbox{ and }\quad\mathsf{swap}^{Γ;X;Y;Δ}_{•} = \mathsf{wait}_Y^{Γ,Y^{•},Ψ}.$$

Swaps are self-inverses.

Let us prove that they are self-inverses; we do so with the negatively-polarized one (<Ref>), the other case is analogous.
We reason using naturality of linking, (i,iv), that shuffles compose as shuffles (ii,iii) (<Ref>), the interaction between shuffling and spawning (v),  and the duality between spawning and linking (vi).

We can link sooner or later without changing the result. Formally, the equations in <Ref> hold.

Linking sooner or later does not change the restult.

We will prove the first one (<Ref>), the second one follows analogously.
We reason using (i) the definition of $\mathsf{wait}$; (ii,iii) that shuffles compose as shuffles (<Ref>); (iv) naturality of linking; and (v) that swaps are self-inverses (<Ref>).

Proof of <Ref>.

Any spawning factors as the spawning of a single channel followed by a shuffling. Formally,

$$\SPW_X^{Γ,Δ}(m) = \SHF_{Γ,X^{∘},X^{•},Δ}(m, \SPW_X^{;}(\NOP)).$$

This is a direct consequence of Axioms (3a,3b).

Theoretically, it would be possible to reason with  at the level of derivations.
However, as we have done through this text, we will try to find better categorical semantics and a better combinatorial expression of the free .
We will be most interested in the categorical semantics of  and how do they interplay with process theories, in the sense of . We introduce specialized semantics in terms of , which are another instance of the idea of partially representing a . For all of this, we will need a coherence theorem.

§.§ Coherence for Message Theories

are not perfectly coherent: easily, we can find that there are two formally well-typed structure maps $A ⊗ A → A ⊗ A$, the identity and the swap. However, what is indeed true is that any two distinctly typed structure maps in the free  are equal. “Distinct typing” is a notion that only makes sense in the free  over some generators; it means that the generators comprising the lists that are our objects appear only once with each variance: arrows $A ⊗ B ⊗ C → B ⊗ C ⊗ A$ are distinctly typed, but arrows $A ⊗ A → A ⊗ A$ are not, because $A$ appears twice with each variance.

Shufflings satisfy a similar form of coherence: there is a unique way of shuffling two words into a third one if these words are distinctly typed.
This section proves that  satisfy the same form of coherence. It is not true that any two parallel formal arrows are equal in any : for instance, there are two ways of deriving $X^{∘},X^{∘}$ from $X^{∘}$ and $X^{∘}$. It is true, however, that there is a unique arrow for any distinctly typed domains and codomain.

are coherent. In the free  over a set of objects, there is at most a single derivation between any distinctly typed premises and conclusion.

Consider distinctly typed premises and conclusion. There must be three different classes of types in this derivation: (1) those that appear twice on the conclusions with different polarity, (2) those that appear twice on the premises with different polarity, and (3) those that appear once in the premises and once in the conclusions with the same polarity.

We will construct a non-unique normal form for derivations in a message theory, taking into account each one of these cases.

* In the first case, the types must have been created by spawning a channel. Using naturality of spawning (Axioms 3a, 3b, 5c), we can move these spawning operations to be shuffled at the end of the derivation. Note that it is not true that we can move all spawning to the end of the derivation, but if the types appear only in the conclusions, then we can always do so.

* In the second case, these variables must get linked to each other. We can always move the linkings to the end of the derivation (before spawning new objects) using again the naturality of the linkings (Axioms 2a, 2b, 5a).

* For the third case, only a shuffling, rushing and waiting can be involved (any linking or spawning that does not involve rushing or waiting has already been moved to the end). Rushing and waiting can be moved to the beginning of the derivation because of naturality of spawning and linking (Axioms 2a, 2b, 3a, 3b).

All of this argues that we can always factor a derivation in a  as (i) rushing and waiting, (ii) a shuffle, (iii) linkings, (iv) spawnings and shufflings of new variables; but we have not yet shown that this derivation is unique.

Imagine that we know the premises $(Γ₁, …, Γₙ)$ and the conclusion $(Δ)$ of a derivation in a . Let us argue that there is at most a unique derivation between these two.

* Removing the objects that appear twice in the conclusion $(Δ)$, we obtain a new conclusion $(Δ₁)$; there is, at most, a unique way of getting from $(Δ₁)$ to $(Δ)$ using spawnings and shufflings: spawning all the possible variables in any order and employing the only possible shuffle (using <Ref>, axioms 1a, 1b, 1c); the order of spawning does not matter because shuffles are symmetric (Axioms 1c, 5c).

* Adding all of the objects that get linked and appear twice with different polarities on the premises, in any order, we obtain a new conclusion $(Δ₂)$. There is a unique way of getting from $(Δ₂)$ to $(Δ₁)$ because of the interchanging axioms of linking (Axioms 5b and 5d). The only obstruction to uniqueness here is that we could choose different conclusions $(Δ₂)$ depending on where they place the variables that will be linked; however, we have already shown that all possible choices lead to the same result (<Ref>).

* We are left with a shuffle and some rushings and waitings.  From the conclusion $(Δ₂)$ we obtain now a sequence of premises $(Γ₁',…,Γₙ')$ that are the same as the original premises $(Γ₁,…,Γₙ)$ with the only difference that the objects appear ordered as in the conclusion $(Δ₂)$. There is a unique possible shuffling from $(Γ₁',…,Γₙ')$ to $(Δ₂)$.

* Finally, for each premise, there will be rushings and waitings. Rushings and waitings interchange (<Ref>), and so there is a unique way of going from the original premise $Γᵢ$ to the new premise $Γᵢ'$.

A summary of the proof can be found in <Ref>: $Δ₁$ is determined from $Δ$; $Δ₂$ is not, but all the possible choices lead to the same result (<Ref>); $Γ₁',…,Γₙ'$ are determined from $Δ₂$ and $Γ₁,…,Γₙ$; we have argued that in each one of the steps of the proof there is a single possible derivation.

Schema for the proof of uniqueness.

§.§ Bibliography

Honda pioneered binary session types in the 90s <cit.>; and further work with Yoshida and Carbone extended them to the multi-party case <cit.>. Session types <cit.>
are the mainstay type formalism for communication protocols, and they have been extensively applied to the π-calculus <cit.>.
Our approach is not set up to capture all of the features of a fully-fledged session type theory <cit.>. Explicitly, our framework of  can be compared to asynchronous session types without choice.
Arguably, this makes it more general: it always provides a universal way of implementing send $(\Send{A})$ and receive $(\Get{A})$ operations in an arbitrary  represented by a .
For instance, recursion and the internal/external choice duality <cit.> are not discussed, although they could be considered as extensions in the same way they are to monoidal categories: via trace <cit.> and linear distributivity <cit.>.

§ PHYSICAL MONOIDAL MULTICATEGORIES, AND SHUFFLINGS

are  <cit.> where the parallel tensor $(⊗)$ is not representable. They follow the same idea of , but they will be a better framework for message passing. The theory of  will need of three ingredients: (i) , which correspond to the symmetry of the parallel tensor $(⊗)$; (ii) , which correspond to the half-representable sequential tensor $(⊲)$; and (iii) normality, which we will need to reinterpret in this setting.

§.§ Symmetric Multicategories

Symmetric multicategories <cit.> are to  what  are to .
Let us write $σ ∈ S(n)$ for an element of the permutation group on $n$ points. Let us write $σ₁ + σ₂ ∈ S(n + m)$ for the disjoint union of two permutations, $σ₁ ∈ S(n)$ and $σ₂ ∈ S(m)$. Let us write as $σ \wr (k₁, …, kₙ) ፡ k_{σ1} + … + k_{σn} → k_1 + … + k_n$ the thickening of a permutation $σ ∈ S(n)$ to a permutation $S(k_1 + \dots + k_n)$ that applies it considering each block of $k_n$ elements separately.

A symmetric multicategory is a  $𝕄$ together with the following family of functions

$$σ^\ast ፡ 𝕄(X_{σ1}, … , X_{σn} ; Y) → 𝕄(X₁, …, Xₙ; Y),\mbox{ for each } σ ∈ S(n),$$

that moreover satisfy the following axioms: (i) functoriality, $(τ ⨾ σ)^\ast(f) = τ^\ast (σ^\ast (f))$ and $\id^\ast(f) = f$; (ii) preservation of disjoint unions, $σ₁^\ast(f_1)⨾_1 … ⨾_{n-1} σ_n^\ast(fₙ) ⨾_n g = (σ₁ + … + σₙ)(f₁ ⨾_1 … ⨾_{n-1} fₙ ⨾_n g)$; and (iii) naturality, $f₁ ⨾_1 … ⨾_{n-1} fₙ ⨾_n σ^\ast(g) = (σ \wr (k₁,…,kₙ))^\ast (f_{σ1} ⨾_1 … ⨾_{n-1} f_{σn} ⨾_n g),$ for any $fₙ$ having arity $kₙ$.

In , symmetry appears with the non representable parallel tensor $(⊗)$; while the sequential tensor will still form a representable , this is the notion of .

§.§ Monoidal Multicategories

helped us describe typed algebras: the objects of the  were the types, and the multimorphisms were the operations we were allowed to use in that algebra. As we saw with , we need a second dimension if we want to study parallelism: what happens when the types themselves form a monoid?  are the monoidal version of algebra.

A monoidal category was a 2-monoid on the 2-category of categories, functors and natural transformations. Analogously, a monoidal multicategory, sometimes called a virtual duoidal category <cit.> or monoidal operad, is a 2-monoid of the 2-category $\Mult$ of multicategories, multifunctors, and multinatural transformations.

A monoidal multicategory $(𝕄,⊲,N,m,i,⨾)$ is a  $(𝕄,⨾)$ with a tensor and a unit both on objects $(⊲) ፡ 𝕄_{obj} × 𝕄_{obj} → 𝕄_{obj}$ and $N ፡ 𝕄_{obj}$, and a tensor and unit on multimorphisms,

\begin{align*}
mₙ ፡ & 𝕄(X₁,\mydots, Xₙ; Y) × 𝕄(X'_1,\mydots, X'ₙ; Y) %
→ 𝕄(X_1 ⊲ X'_1, \mydots, Xₙ ⊲ X'ₙ; Y ⊲ Y'), \\
n_n ፡ & 1 → 𝕄(N, \overset{n}\dots, N; N).
\end{align*}

These are associative and unital up to multinatural transformations $α_{X,Y,Z} ∈ 𝕄(X ⊲ (Y ⊲ Z); (X ⊲ Y) ⊲ Z)$, $λ_X ∈ 𝕄(I ⊲ X; X)$ and $ρ_X ∈ 𝕄(X ⊲ I; X)$, satisfying the pentagon and triangle equations.

Any  has an underlying .
Multifunctors between representable multicategories are lax monoidal functors, and multinatural transformations are lax monoidal transformations. This implies that a representable monoidal multicategory is exactly a  <cit.>.

§.§ Physical Monoidal Multicategories

Bringing the notion of normality to the context of  is not completely trivial: here, there is no map between the two units $I → N$. Instead, what we will have is a map between the hom-sets, given by the precomposition of the multimap $n₀ ∈ 𝕄(;N)$ that we have because of the monoidality of the unit.

A physical monoidal multicategory is a  $(𝕄,⨾,\id)$ that is moreover monoidal forming a virtual duoidal category $(𝕄,⊲,N)$ and that contains an invertible composition with the unit map.
That is, the following composition is an isomorphism,

$$(n₀ ⨾ •)^{-1} ፡ 𝕄(X₀,\overset{n}{…},Xₙ ; Y) → 𝕄(X₀,…,N,…,Xₙ; Y).$$

We know the structure we need, but we will need to be able to compute with it.
A better combinatorial description of  will be possible once we characterize the free ones.
The next section shows that the  of shufflings is the free normal symmetric monoidal multicategory over a set of objects.

§.§ Shuffling

Shuffling events is the principle on which we have based our definition of .
The first step towards endowing them with categorical semantics is to show that shuffling arises naturally in a categorical setting: if  represented inclusions of posets,  will represent inclusions of linear posets, which correspond to shuffling.

Let $A$ be an alphabet. The  of shuffling words, $\mathsf{wShuf}_A$, has as objects the set $A^\ast$ of words on the alphabet $A$. The multimorphisms $\mathsf{wShuf}_A(w₁,…,wₙ; w)$ are precisely the shufflings of the letters of the words $w₁,… , wₙ$ that result into the word $w$. The monoidal tensor is given by concatenation of words.

This  is not posetal: for instance, there exist two multimaps $\mathsf{wShuf}_A(a,a;aa)$ for any letter $a ∈ A$. More generally, the number of shuffles of a repeated letter is given by the binomial coefficients,

\[\#\mathsf{wShuf}(a^{n_1},…,a^{n_k}; a^{n₁ + … + nₖ}) = \frac{(n₁ + … + nₖ)!}{n₁! … nₖ!}.\]

However, it is true that, if each letter appears at most once on the component words, then the shuffle, if it exists, must be unique. For instance, there exists a unique shuffle $\mathsf{wShuf}(xy,wz; xwyz)$, and so we can refer to it without explicitly specifying it. In other words, there exists at most one morphism between formal distinctly-typed expressions; shuffles are coherent.

This  is symmetric and normal. In other words, it is a .

are the free  on a set of objects.

We have already shown how they form a ; we need to show that it is the free one. Let $𝕍$ be any , for each map $A → 𝕍_{obj}$ there must exist a unique physical monoidal multifunctor $\wShuf_A → 𝕍$ that factors on objects through the former map.

First, we argue that the physical monoidal multifunctor is forced. Any shuffle can be reconstructed from the operations of a , and so any shuffle must be mapped accordingly. For instance, if we want to reconstruct the shuffle $𝕍(xy,z; xzy)$, we multiply together: first $𝕍(x,i;x)$, then $𝕍(i,z;z)$, and finally $𝕍(y,i;y)$.

Let us do this in general. Assume a shuffle $\wShuf(w₁,…,wₙ; w)$, where the words are $wⱼ = a_{j,1} … a_{j,k_j}$. We position each one of the letters in their position: for instance, if $a_{j,i}$ appears in the $j$th-word, we can use the normalization isomorphism

$$𝕍(a_{j,i};a_{j,i}) ≅ 𝕍(I,…,a_{j,i}^{(j)},…,I; a_{j,i})$$

to position it in the $j$th input, via the identity multimorphism. Then, we can multiply all of the letters forming the shuffle, using monoidality, and obtain the desired shuffle in any ,

\[ \prod_{a_{j,i} ∈ w} 𝕍(I,…,a_{j,i}^{(j)}, …,I ; a_{j,i}) \rightarrow 𝕍(w₀,…,wₙ; w).\]

We have used exactly one factor for each letter of the resulting word.

Finally, we need to prove that this assignment is well-defined and that it defines a physical monoidal multifunctor. These will be both a consequence of the same fact: there exists at most a unique shuffle between words with different letters and there exists at most a unique formally distinctly typed map between any poset shapes.
To prove this, we use the characterization of the free duoidal category as poset shapes: there is a single formally well-typed map between any two poset shapes, so there is a single formally well-typed map between any two duoidal expressions; in particular, there exists at most one multimorphism between any words with distinct letters in a physical monoidal multicategory.
This renders the map well-defined: there is at most one way of constructing any shuffle, and we have shown that it is possible. On the other hand, this also makes the map a physical monoidal multifunctor: all the equations are formal and thus they hold automatically.

Shuffling takes care of the first and most important aspect of message theories:  are algebras for the shuffling words  of their objects.
However, message theories do have an extra structure: each object is a left dual, naturally with respect to these shufflings – the second ingredient for message theories is polarization.

§.§ Bibliography

This formulation of  is a particular case of Shulman's definition of  over a faithful cartesian club <cit.>. The theory of  is less developed than the theory of cartesian multicategories, which are well-known to correspond to Lawvere theories.
are also not particularly explored, but Shulman has a note relating them directly to  and proposing the name virtual duoidal category for them <cit.>.

§ POLARIZATION

Polarization is not a property of our structures, but more of a particular way of constructing free structures. This is, we do not say that a monoid is “polarized”; but we have constructed free polarized monoids when talking about . Saying that a monoid is polarized would seem to imply that all of its elements have a sign, which is not what happens in the free polarized monoid: generators do appear with a sign, but the words on the monoid are combinations without a particular sign.

Given any monoid $M$, we can consider its polarization, $\mathsf{Polar}(M)$, to be the monoid generated by two copies of each element of $M$, denoted $a^{•} ∈ \mathsf{Polar}(M)$ and $a^{∘} ∈ \mathsf{Polar}(M)$, and quotiented by the equations $a^{•} b^{•} = (ab)^{•}$ and $a^{∘}b^{∘} = (ab)^{∘}$.

Taking seriously this idea, we will not regard polarization as part of an algebraic structure (as it happens with ). Instead, polarization will arise as a left adjoint. To quip, polarization is left adjoint to taking left adjoints. Let us see first how this works in the context of monoidal categories; we will later extend it to .

§.§ Monoidal Polarization

Every  has a notion of duality inside it. It does not suffice to say that some objects have duals: a duality is not only a property. Instead, we need to specify the maps that constitute the duality. Dualities in a  form a  themselves. Polarization is the left adjoint to taking this category of dualities.

Let $(ℂ,⊗,I)$ be a monoidal category.
We define the category of left duals, $\mathsf{Duals}(ℂ)$ to have objects the dualities $(L ⊣ R, ε, η)$ of the monoidal category and morphisms

$$(f_L,f_R) ፡ (L ⊣ R, ε, η) → (L' ⊣ R', ε', η')$$

to be pairs of morphisms $f_L ፡ L → L'$ and $f_R ፡ R' → R$ such that the equations in <Ref> hold.

Morphism of adjunctions.

The category of left duals is a monoidal category where the tensor of two dualities, $(L ⊣ R, ε, η)$ and $(L' ⊣ R', ε', η')$, is defined to be

$$(L ⊗ L' ⊣ R' ⊗ R, (\id ⊗ ε ⊗ \id)⨾ ε', η ⨾ (\id ⊗ η ⊗ \id)).$$

Taking the left duals extends to an endofunctor $\mathsf{Duals} ፡ \mathbf{MonCat} → \mathbf{MonCat}$.
This endofunctor has a right adjoint $\mathsf{Polar} ፡ \mathbf{MonCat} → \mathbf{MonCat}$.

Let $(ℂ,⊗,I)$ be a strict monoidal category.
Its polarization, $\mathsf{Polar}(ℂ)$, is a monoidal category presented by the following data.

The polarization contains two objects, $A^{•}$ and $A^{∘}$, for each object of the original category $A ∈ ℂ_{obj}$, and quotiented by equalities for tensors $(A ⊗ B)^{•} = A^{•} ⊗ B^{•}$ and $(A ⊗ B)^{∘} = B^{∘} ⊗ A^{∘}$ and units $I^{•} = I^{∘} = I$.
It also contains a pair of morphisms $ε_A ፡ A^{•} ⊗ A^{∘} → I$ and $η_A ፡ I → A^{∘} ⊗ A^{•}$ constructing an adjunction $A^{•} ⊣ A^{∘}$: that is, $ε_A ⨾ η_A = \id$ and $η_A ⨾ ε_A = \id$. The duality is monoidal, satisfying both $ε_{A ⊗ B} = ε_A ⨾ ε_B$ and $η_{A ⊗ B} = η_B ⨾ η_A$, and finally $ε_I = η_I = \id_I$.

The polarization contains two dual morphisms, $f^{•} ፡ A^{•} → B^{•}$ and $f^{∘} ፡ B^{∘} → A^{∘}$, for each morphism $f ፡ A → B$.  These are quotiented by equations explicitly asking for functoriality: $f^{•} ⨾ g^{•} = (f ⨾ g)^{•}$ and $\id^{•} = \id$, and also $f^{∘} ⨾ g^{∘} = (g ⨾ f)^{∘}$ and $\id^{∘} = \id$.  These are tensored as $(f ⊗ g)^{•} = f^{•} ⊗ g^{•}$ and $(f ⊗ g)^{∘} = g^{∘} ⊗ f^{∘}$.

Polarization is left dual to taking left duals.

We already know that $\Duals ፡ \MonCat → \MonCat$ is a functor; we only need to construct a universal arrow $η_{𝕄} ፡ 𝕄 → \Duals(\Polar(𝕄))$. The universal arrow will be given by $η(X) = (X^{•} ⊣ X^{∘}, ε_X, η_X)$, which uses the fact that $X^{•} ⊣ X^{∘}$ determines an adjunction. This assignment extends to a functor that sends a morphism $f ፡ X → Y$ to a morphism of dualities $(f^{•}, f^{∘}) ፡ (X^{•} ⊣ X^∘{}, ε, η) → (Y^{•} ⊣ Y^{∘}, ε, η)$, where $f^{∘} ፡ Y^{∘} → X^{∘}$ is the dual of $f^{•} ፡ X^{•} → Y^{•}$. This constructs the candidate universal arrow.

Let us show that it is indeed universal. Consider a functor $H ፡ 𝕄 → \Duals(ℕ)$. We will show that there is a unique $H^\ast ፡ \Polar(𝕄) → ℕ$ such that $H = η_{𝕄} ⨾ \Duals(H^\ast)$. Let us pick an object $X ∈ 𝕄_{obj}$ that is sent to $H(X) = (A ⊣ A', ε_A, η_A)$.  To make this equation hold, it is necessary that $H^\ast(X^\circ) = A$ and $H^\ast(X^\bullet) = A'$, but also $H^\ast(ε_X) = ε_A$ and $H^\ast(η_X) = η_A$.
Let us pick a morphism $f ፡ A → B$ that is sent to $H(f) = (g_L,g_R) ፡ (A ⊣ A', ε_A, η_A) → (B ⊣ B', ε_B, η_B)$; this forces $H^\ast(f^{•}) = g_L$ and $H^{\ast}(f^{∘}) = g_R$.
Because $(A ⊣ A', ε_A, η_A)$ forms a duality and the maps $g_L$ and $g_R$ are duals, this assignment satisfies all necessary equations.
This determines the value of $H^\ast$ on all of the generating maps while satisfying all of the equations of $\Polar(𝕄)$.

§.§ Monoidal Polarization is Not Enough

An important insight of some works into the categorical semantics of message passing is the importance of polarization. Given this, one could expect that the polarization of a  is its corresponding .
Indeed, this chapter will claim that the polarization of a  exhibits the necessary structure to discuss message passing; however, at the same time, it will claim that the algebraic structure that allows it to do so is not that of a polarized monoidal category: it is that of a .

Some simpler interleavings of events can be expressed using dualities in a . For instance, let us consider the polarization of a : wires with the same sign can be swapped, but wires with different sign cannot. We can interleave two maps $f ፡ I → X^{∘} ⊲ Y^{∘} ⊲ Z^{•}$ and $g ፡ I → U^{∘} ⊲ V^{•}$ to produce a map $h ፡ I → X^{∘} ⊲ U^{∘} ⊲ V^{•} ⊲ Y^{∘} ⊲ Z^{•}$ as in <Ref> – note how we use the adjunction to contort the wires and allow wires to pass over wires with different polarization.

A shuffling, using polarization.

In general, thanks to the dualities, a receiving resource can be used later, $X^{∘} ⊲ A → A ⊲ X^{∘}$, and a sending resource can be sent sooner, $A ⊲ X^{•} → X^{•} ⊲ A$, but not the other way around. These two laws govern which wires can pass over other wires. A natural question, then, is to ask if all possible interleavings can be expressed in the same way: polarizing objects, and using dualities.

It is not the case that every shuffling of events can be expressed in a category with polarized objects and dualities.

Consider two cells as in <Ref>, with types

\begin{align*}
f ፡ I → X^{•} ⊲ Y^{∘} ⊲ Z^{•} ⊲ W^{∘}, \mbox{ and }
g ፡ I → A^{•} ⊲ B^{∘} ⊲ C^{∘} ⊲ D^{•} ⊲ E^{•} ⊲ F^{∘}
\end{align*}

and imagine we want to interleave them into $A^{•} ⊲ B^{∘} ⊲ X^{•} ⊲ Y{∘} ⊲ C^{∘} ⊲ D^{•} ⊲ Z^{•} ⊲ W^{∘} ⊲ E^{•} ⊲ F^{∘}$ using only the dualities. There are two possible cases: (i) we place $f$ before $g$ and we try to position the wires of $f$ correctly; or (ii) we place $g$ before $f$ and we try to do the same.

In the first case, we will find that we can pass the wire $X^{∘}$ over $A^{•} ⊲ B^{∘}$ – but the same cannot be done with the wire $Y^{•}$. Therefore, we are forced to pass the wire $Y^{•}$ over $C^{∘} ⊲ D^{•} ⊲ E^{•} ⊲ F^{∘}$, using the dualities; but then there will be no way of moving the wire $Z^{•}$ to its place.

A shuffling that cannot be expressed.

In the second case, the first two wires, $A^{•} ⊲ B^{∘}$, are automatically correctly placed. The third, $C^{∘}$, must pass over $Z^{•} ⊲ W^{∘}$ because it could not do the same with $X^{•} ⊲ Y^{∘}$; so $D^{•}$ would be forced to do the same, but it cannot.

Then, if this algebra is not what we are using about the polarization of a , what are we using exactly? It happens that the polarization of a  posesses extra structure: its states (the morphisms without input) can always be split into morphisms that take negative objects on the left and produce positive objects on the right. This property is what makes it possible to express any interleaving of events.

With this in mind, the polarization of a  seems interesting not only because it produces a category with duals (or, in the work of Nester <cit.>, a proarrow equipment, or a cornering), but because it constructs a full . We do not only care about the free polarization, we care about its .

§.§ Polarization of a Physical Monoidal Multicategory

Every  has a notion of dual, inherited from that of its underlying monoidal category. The next section will construct the free polarized  over a set of objects. Let us define here the right adjoint: the functor that picks the set of left adjoints of a .

Let $(𝕄,⊲,I)$ be a .  We define the set of left duals, $\Duals(𝕄)$, to have objects the dualities $(L ⊣ R, ε, η)$ where $ε ∈ 𝕄(L ⊲ R; I)$ and $η ∈ 𝕄(I ; R ⊲ L)$ are 1-to-1 multimorphisms satisfying the adjoint equations, $(ε ⊲ \id_L) ⨾ (\id_R ⊲ η) = \id_L$ and $(\id_R ⊲ ε) ⨾ (η ⊲ \id_R) = \id_R$.

§.§ Bibliography

A categorical treatment of polarization appears in the work of Cockett and Seely <cit.>, which points to the connection with Abramsky-Jagadesaan games <cit.>. “Polarized category” takes a different meaning there: it is a pair of categories endowed with a  between them. However, we do follow the same core idea: using walking adjunctions for sending and receiving.

Nester notices the importance of polarization for message passing <cit.> via a single-object proarrow equipment; and all the credit for this idea should go there. This was later extended by Nester and Voorneveld <cit.> to include iteration and choice.
The reader will find a discussion of its relationship with lenses in a joint paper of this author with Nester and Boisseau <cit.>.
The graphical calculus of proarrow equipments was described by Myers <cit.>; we can reuse this calculus to explain polarization in .
Here, we prefer to avoid discussing polarization through proarrow equipments, noticing that this adjunction already works at the level of .

§ POLAR SHUFFLES

§.§ Polar Shuffles

Polarization in a  leads us to consider : shufflings endowed with a polarization for each one of its elements. This section will show that  are the free polarized .

The objects of the category of shuffles could be seen as the finite ordinals: finite linear posets with inclusions on each other, preserving the ordering. Similarly, the objects of the category of  are polarized finite ordinals.

A polar list over a set of types $T$ is a list of types $X ∈ T^\ast$ endowed with a function $p ፡ X → \{ ∘, • \}$.
In any polar list, we consider the negative elements, $X^{∘} = p^{-1}(∘)$, and the positive elements, $X^{•} = p^{-1}(•)$.

A polar shuffle over a set of types $T$, from a multiset of polar lists $X₀,…,Xₙ$ to a single polar list $Y$, is a bijection

\[f ፡ X₁^{•} + … + Xₙ^{•} + Y^{∘} → Y^{•} + X₁^{∘} + … + Xₙ^{∘}\]

preserving the types and such that the directed graph containing all polar lists (as linear posets) and an edge $x → f(x)$ for each element in $X₁^{•} + … + Xₙ^{•} + Y^{∘}$, is acyclic.

For instance, an untyped  (or typed over the singleton set) of shape $\pShuf({∘}•{∘}•, {∘}{∘}••, {∘}; {∘}{∘}••{∘})$, is given by the following acyclic graph in <Ref>. In black, we depict the edges that come from the graph of a function. In blue, the edges that come from the linear finite posets.

A polar shuffle.

§.§ Encoding of polar shuffles

are ultimately graphs, and they can be encoded as such. We propose a notation suggestive of multiparty session calculi.

The session encoding of  assigns a variable name to each polar list (say, $f, g, h, …$) and to each edge of the graph outside a polar list (say, $a,b,c,x,y,z,…$). The encoding of a  starts by declaring the list of edges incident to the output polar list, together with their polarization. Then, enclosed in braces, we write the polar lists and the edges that incide on them.

For instance, the encoding of the  in <Ref> is in <Ref>.

Encoding of a polar shuffle.

Parsing this notation requires checking whether the graph is acyclic. Checking if a graph is acyclic can be done in linear time on the sum of vertices and edges, $𝓞(v+e)$. The number of vertices in a  is the sum of the lengths of all of the polar lists involved, $e = \#X₁ + … + \#Xₙ + \#Y,$ and each vertex receives at most three edges, giving a bound $e \leq 2v$. This means that checking if a  is valid is linear in the length of its polar lists, $𝓞(\#X₁ + … + \#Xₙ + \#Y)$.

The second implication of this encoding is that, if we label the vertices of a  with types, there exists at most one  with any distinctly typed sources and targets.

are coherent. There exists at most a single  between some distinctly typed polar lists: we say that a polar list is distinctly typed if each variable (each type) appears in the premises and the conclusion exactly twice, each time with a different variance.

In this combinatorial structure, coherence works almost by definition.
Note that a  is ultimately a bijection satisfying certain extra properties; but the distinct typing already forces where each element must be sent: to the only element with different variance but same type. Whether the  exists at all depends on whether it satisfies the acyclicity property.

§.§ The Multicategory of Polar Shuffles

form a , as their shape already suggests. The composition and the rest of the structure follow that of the category of shufflings. For instance, the composition of  is defined to be the substitution of the resulting polar list of a shuffle into the input polar list of another shuffle. See <Ref> for an example.

Composition of two polar shuffles.

The composition of two , $s ∈ \pShuf(X₁,…,Xₙ;Y)$ and $t ∈ \pShuf(Y_1,…,Y,…,Yₘ;Z)$, along a polar list $Y$, is a  obtained by substituting the entire graph of the former into the polar list of the latter,

$$s ⨾_Y t ∈ \pShuf(Y_1,…,X₁,…,Xₙ,…,Yₘ;Z).$$

Substituting a  into the inputs of a  forms again a . That is, composition is well-defined and preserves acyclicity.

Composition happens across the resulting polar list of a , which coincides with one of the input polar lists of another ; we say that this polar list is the border. The proof argues that two acyclic graphs glued along a linear graph are again acyclic.

Let us prove this by contradiction. Imagine there was a cycle in the multicategorical composition of . It must contain edges on both components of the composition, simply because each component is itself acyclic. This means that the cycle should cross the border between both components of the  at least twice and always an even number of times – it must take two different directions.

Composition along the borders of two polar shuffles.

Because the border is a linear poset, it must split the cycle (at least) in two parts, creating two undirected cycles to the two sides of the border. At least one of these two is forced to be directed, thus contradicting acyclicity on that side of the composition.

The tensoring of two polar shuffles of the same arity,

$$s ∈ \pShuf(X₀,…,Xₙ;Y)\mbox{ and }t ∈ \pShuf(X'₀,…,X'ₙ;Y'),$$

is a polar shuffle on the pointwise concatenation of the polar lists

$$(s ⊲ t) ፡ \pShuf(X₀X'₀,…,XₙX'ₙ;YY'),$$

defined by the disjoint union of the two acyclic graphs determining the polar shuffles.
The tensoring of two polar shuffles is well-defined and it is again a polar shuffle.
See <Ref> for an example.

Parallel composition of polar shuffles.

The graph of the tensoring is the disjoint union of two acyclic graphs, together with the edges determined by the polar lists. The directed edges coming from the polar lists always go from the first graph to the second; thus, they will not create cycles and the resulting graph with be acyclic.

Polar shuffles over a set of types are the morphisms of a , $\pShuf{}$, that has the polar lists as objects.

We define the identity polar shuffle on a polar list to be the identity bijection linking each sign to itself. The identity polar shuffle is acyclic because the identity bijection preserves the linear ordering. We have already defined the composition and shown that it is acyclic in <Ref>. Associativity of composition follows from associativity of glueing graphs; unitality follows by construction. We have already defined the tensoring in <Ref>, and the tensor on objects is the concatenation of polar lists. The unit for the tensoring is the empty polar list, and because it does not appear in a , it makes the  normal.

§.§ Message Theories are Algebras of Polar Shuffles

What makes  relevant to the discussion of message-passing is that they promise us a better syntax for . Instead of thinking of the operations of a  as generated by a few primitives satisfying equations, we can give them a combinatorial characterization in terms of . This section shows that  are precisely the algebras for the operations given by .

An algebra over a , $(𝕄,⨾,\id)$, is the assignment of a set $S(X)$ to each object $X ∈ 𝕄_{ob}$, and the assignment of a function

\[S(f) ፡ S(X₁) × … × S(Xₙ) → S(Y),\]

for each multimorphism $f ∈ S(X₁, …, Xₙ; Y)$.  The assignment must preserve compositions, $S(f ⨾_X g) = S(f) ⨾_X S(g)$ and identities, $S(\id) = \id$. Alternatively, it is a multifunctor to the cartesian monoidal category of sets and functions.

are precisely the algebras of the free polarized  over their respective sets of types. In other words, the derivations of a  form the free polarized  over its set of types.

This will follow almost by definition. The definition of  includes an operation for each shuffling, and these operations compose as shufflings (<Ref> and Axioms 1a, 1b, and 1c); equivalently, this is saying that  are in particular algebras of the multicategory of shufflings, the free  over their set of types.

The rest of the axioms of  are exactly asking that each object is a left adjoint: the spawning and linking operations are describing the unit and the counit of the adjunction; the rest of the axioms are saying that: the unit of the adjunction is natural with respect to shufflings (Axioms 2a and 2b); the counit of the is natural with respect to shufflings (Axioms 3a and 3b); unit and counit satisfy the snake equations (4a and 4b); and they are natural with respect to each other (Axioms 5a, 5b, 5c and 5d).

Polarized  are coherent; there exists at most one multimorphism between any distinctly typed objects of the free  over some objects.

This is now a consequence of <Ref> and <Ref>. The derivations of a  form the free polarized , but we have already shown that they are coherent.

form the free polarized  over a set of types.

are coherent (<Ref>), and polarized  are coherent as well (<Ref>); this simplifies the proof because, to show that they coincide, we only need to show that a  between some types exists if an only if a multimorphism in the free polarized  exists.

If a multimorphism of a certain type exists in the free polarized , then it exists in all polarized  and, in particular, in  (<Ref>).

Let us prove the converse implication: if a  between some types does exist, then there is a multimorphism in the free polarized  between these types. For this, we will use that a can be always factored (not necessarily uniquely!) in the following way: (i) we exchange positions inside each polar list to get them to their final relative position; (ii) we use a series of spawnings, or polar shuffles $I → X^{∘} ⊲ X^{•}$; (iii) we use a pure, non-polarized shuffle; and (iv) some final linkings of type $X^{•} ⊲ X^{∘} → I$. This is easy to verify topologically: we can always `pull down the linkings' and `pull up' the spawnings, and we can always factor any shuffle in two parts – a pure shuffle and a shuffle internal to each one of the components. For instance, consider the following example in <Ref>, adapted from <Ref> with an extra spawning.

Factored polar shuffle.

Spawning, linking, shuffling, waiting and rushing are all operations on a  (see <Ref>); so this proves that there is at least one multimorphism in the free  with these types. We do not care about the specific choice of multimorphism because  are coherent (<Ref>), and polarized  are coherent as well (<Ref>)

are the algebras of the  of .

We will use that  are the free polarized  (<Ref>) and that  are precisely the algebras of the free polarized  over their objects (<Ref>).

§.§ Bibliography