The definition – and the notation – of polar shuffles takes inspiration from a different concept: Hughes' partial leaf functions <cit.>. Partial leaf functions are the $\mathbf{Int}$-construction – the free compact closed category over a traced monoidal category – applied to the category of finite sets and partial functions <cit.>; here we follow a similar idea, but we work over finite sets and bijections, which are not traced. Not only the $\mathbf{Int}$-construction, but also the idea of shuffling two traces point back to game semantics <cit.>.

§ PROCESSES VERSUS SESSIONS

§.§ Processes of a message theory

Inside of a , we call processes the sessions that happen in two parts: (i) first they ask for some indeterminate number of resources (possibly zero), $X₁^{∘},…Xₙ^{∘}$ and (ii) then, they give some indeterminate number of resources (possibly zero), $Y₁^{•},…,Yₘ^{•}$. This simple definition builds a  inside any , and we will find a left adjoint to this construction.

Let $𝕄$ be a . There exists a , $\mathsf{Proc}(𝕄)$, whose objects are the lists of objects of the , $\Proc(𝕄)_{obj} = 𝕄^\ast_{obj}$, and whose morphisms are the sessions that first ask some resources and then provide some resources,

$$\Proc(𝕄)(X₁ ⊗ … ⊗ Xₙ; Y₁ ⊗ … ⊗ Yₘ) = 𝕄(X^?_n,…X^?_1; Y^!_1,…,Y^!_m).$$

Note how we reverse the order of inputs; this will make reasoning easier even if it is unnecessary: the monoidal category will be symmetric in any case.

Let us define the composition and identities. Composition is given by the  that connects the middle outputs to inputs, see <Ref>; because  are algebras of , such a  defines an operation, composition, that takes two sessions to a third one.

Composition of processes of a message theory.

Identities are created by spawning channels, see <Ref>. Again, because  are algebras of , each  must contain a constant given by the  that spawns a list of channels.
Composition and identities are associative and unital: it can be checked from the definition that we are using the duality from spawning and connecting channels.

Identity process of a message theory.

Symmetries are given by the polar graph that spawns a channel for each one of the objects and then shuffles them so that the inputs and the outputs are divided in two blocks and positioned in reverse order, see <Ref>.

Symmetries of processes in a message theory.

Tensoring is given by the  that preserves all outputs and inputs but passes the outputs of a process pass the inputs of the other, see <Ref>. This operation is again associative and unital with the empty  that represents the monoidal unit.

Tensor of processes in a message theory.

It concludes the proof to check, by following the connections of the , that tensoring behaves functorially with composition so that the interchange law of monoidal categories holds.

The construction of the  of processes extends to a functor

$$\Proc ፡ \mathbf{Msg} → \SymMonCatStr.$$

We will show that any message functor $F ፡ 𝕄 → ℕ$ induces a strict symmetric monoidal functor $\Proc(F) ፡ \Proc(𝕄) → \Proc(ℕ)$. Because the category of processes is freely generated on objects, it suffices to explain that the object $X ∈ 𝕄_{ob}$ is sent to the object $FX ∈ N_{ob}$. On morphisms, we already have a map

$$F ፡ 𝕄(Xₙ^{?},…,X₁^{?},Y₁^{!},…,Yₘ^{!}) → ℕ(FXₙ^{?},…,FX₁^{?},FY₁^{!},…,FYₘ^{!})$$

that gets reinterpreted as a map

$$\Proc(𝕄)(X₁ ⊗ … ⊗ Xₙ;Y₁ ⊗ … ⊗ Yₘ) → \Proc(ℕ)(F(X₁ ⊗ … ⊗ Xₙ);F(Y₁ ⊗ … ⊗ Yₘ)).$$

Composition, identities and tensoring are operations constructed as , and so they must be preserved by a message functor; this means that $\Proc(F)$ becomes a strict monoidal functor.

§.§ Sessions of a process theory

We will now construct message sessions over an arbitrary , and we will do so in a minimalistic theory. Message passing  consists of two effects: sending and receiving.  already are a framework for effectful computation in process theories, so we employ them here.

The  of sessions over a strict  $ℂ$ is the  $ℂ → \Session(ℂ)$ generated by

* all of the morphisms of the original , $ℂ$, quotiented by the equations of the original monoidal category, as pure morphisms;

* and a pair of send and receive generators for each object $X ∈ ℂ_{obj}$ imposing no further equations. We write these generators as $(∘)_X ፡ X → I$ and $(•)_X ፡ I → X$.

Session runtime generators.

This naive theory of message passing on top of a  may remind us of the combs that we were studying before: instead of using incomplete diagrams, we are marking the interchanges explicitly now. This intuition can be made formal: we will now prove that combs of type $X^{‽}_1 ⊲ … ⊲ X^{‽}_n → \pbiobj{A}{B}$ correspond to sessions $A → B$ where the events are exactly $X^{‽}_1, …, X^{‽}_n$, and happen in that specific order. First, note that we can define a sequence of events associated with a particular session.

The sequence of events of a session is the list of effectful generators obtained by following only the effectful wire on the diagram. Formally, it is defined by structural induction over the premonoidal category of sessions as follows.

* It is the empty list for a pure morphism.

* It is invariant to whiskering.

* It contains a single element $[X^{∘}]$ for each generator $(∘)_X ፡ I → X$.

* It contains a single element $[X^{•}]$ for each generator $(•)_X ፡ X → I$.

* It concatenates the lists for a composition of morphisms.

It becomes straightforward to check that the sequence of events is well-defined. We write $\Session(A;B)[X^{‽}_1, …, X^{‽}_n]$ for the set of sessions $A → B$ with a sequence of events $X^{‽}_1, …, X^{‽}_n$.

Sessions from $A$ to $B$ with a sequence of events $X^{‽}_1, …, X^{‽}_n$ are in bijective correspondence with combs with the same events happening sequentially,

$$\Session(A ; B)[X^{‽}_1, …, X^{‽}_n] ≅ \mLens\left( X^{‽}_1 ⊲ … ⊲ X^{‽}_n; \biobj{A}{B} \right).$$

We proceed by structural induction over the presentation of the cteogry of sessions. The base case consists of a morphism that is pure: by definition, those are the combs $\mLens(𝖭; \biobj{A}{B})$.

The inductive case considers a morphism $A → B$ with at least one first occurrence of the effectful generators, $(∘)_X$ or $(•)_X$. We assume without loss of generality that this is $(•)_X ፡ I → X$, so its sequence of events is $X^{•},Γ$ – the other case is analogous.
We consider it as a string diagram for a , quotiented by the equations of the base  $ℂ$, the symmetries and only up to interchange by isotopy.
We may split the diagram into two parts (as in <Ref>); we leave everything before the generator $(•)_X$ to one side, $f ∈ ℂ(A; X ⊗ M)$, and everything after the generator to the other side $g ∈ \Session(M,B)[Γ]$. This procedure constructs the following comb,

$$∫^{M ∈ ℂ} \withPoint{f}{ℂ(A; M ⊗ X)} × \withPoint{g}{\Session(A ; B)[Γ]}.$$

Splitting the diagram of a session.

Of course, the usual problem with this kind of definitions that split a string diagram is that we need to prove that they are well-defined. We need to show that this definition is invariant to isotopy; we do so by cases: (i) if the isotopy interchanges two boxes before the cutting line, then there were two pure morphisms and it is captured by an equation of $ℂ$; (ii) if the isotopy interchanges two boxes after the cutting line, then it is defining an equation of sessions; (iii) if the isotopy interchanges two morphisms across the cutting line, then it is captured by dinaturality.

At the same time, note that these are exactly all of the equations imposed to combs: those of the original  and ; so the correspondence is bijective. Finally, by the induction hypothesis,

\begin{align*}
\Session(A;B)[X^{•},Γ]
& ≅ {\textstyle ∫}^{M ∈ ℂ}\ ℂ(A; X ⊗ M) × \Session(A;B)[Γ] \\
& ≅ {\textstyle ∫}^{M ∈ ℂ}\  ℂ(A; X ⊗ M) × \mLens\left(Γ;\biobj{A}{B}\right) \\
& ≅ \mLens\left(X^{•} ⊲ Γ;\biobj{A}{B}\right),
\end{align*}

which concludes the proof.

The next step is to show that sessions over a  actually define a . For this, we will only need sessions with no inputs or outputs: we write $\Session[Γ]$ for $\Session(I;I)[Γ]$.

Sessions over a strict , $\Session(ℂ)$, form a .
This construction extends to a functorial assignemnt

$$\Session ፡ \SymMonCatStr → \Msg.$$

We will show that sessions over a strict , $\Session(ℂ)$, form an algebra for the  of . Consider a family of sessions, $sᵢ ∈ \Session(Γᵢ)$; and consider a

$$p ∈ \pShuf(Γ₁,…,Γₙ; Δ),$$

we need to construct a new session of type $Δ$.

The construction follows a topological intuition: consider the hypergraph defining the string diagrams of the sessions; and consider at the same time the acyclic graph defined by the . We glue the string diagram of each $sᵢ$, along its runtime wire, to the inputs and outputs, $Γᵢ$, of the , removing these nodes on the process. The crucial step happens now: we have a graph containing nodes of the  of sessions, and it has been constructed by gluing acyclic graphs along linear boundaries – it must be acyclic, and it must be a string diagram.

We define the composition of the sessions $sᵢ ∈ \Session(Γᵢ)$ along the  $p ∈ \pShuf(Γ₁,…,Γₙ; Δ),$ to be the session represented by the string diagram here obtained. This assignment preserves the composition of  – which is also defined topologically by gluing – and thus it determines an algebra.

Finally, the assignment is functorial with respect to the base monoidal category because (i) the construction of the sessions is functorial and (ii) we only apply operations of a symmetric  when we build a string diagram over this  of sessions.

Consider two morphisms, $f ፡ A → M ⊗ X$ and $g ፡ M ⊗ Y → B$, determining a session of type $[A^{∘},X^{•},Y^{∘},B^{•}]$; and consider two other morphisms, $h ፡ X ⊗ U → N$ and $k ፡ N → Y ⊗ V$, determining a session of type $[X^{∘},U^{∘},V^{•},Y^{•}]$.
They can compose along the  we defined in <Ref>; the result is in <Ref>.

Two sessions compose along a polar shuffle.

§.§ Sessions versus Processes

The final result of this section is to prove that sessions over a  are the free  over a .

There exists a strict symmetric monoidal functor
$$\inProc ፡ ℂ → \Proc(\Session(ℂ))$$
that includes a  in the processes of its .

The functor will act as the identity on objects.
We already know that combs are sessions (<Ref>), and we can use this fact to construct the assignment on

\begin{align*}
\Proc(\Session(ℂ)(A;B)) = \Session(ℂ)[A^{∘}, B^{•}]
≅  \mLens(A^{∘}, B^{•}; \biobj{I}{I})
≅ ℂ(A;B).
\end{align*}

It only remains to show that this assignment defines a strict symmetric monoidal functor: we need to show that it preserves composition, tensoring, identities and symmetries. This is straightforward, as we only need to check that the operations that we defined for the  of a , $\Proc(𝕄)$, correspond to the operations of a .
Let us explicitly check composition, $\inProc(f) ⨾ \inProc(g) = \inProc(f ⨾ g)$, in <Ref>, the rest follow a similar pattern.

The inclusion of processes preserves composition.

Checking the rest of the cases concludes the construction.

Sessions and processes form an adjunction, $\Session ⊣ \Proc$; where sessions, $\Session ፡ \SymMonCatStr → \Msg$, construct the free  over a , and where processes, $\Proc ፡ \Msg → \SymMonCatStr$, construct the cofree  over a .

Consider a strict , $ℂ$, and a , $𝕄$, endowed with a strict symmetric monoidal functor $F ፡ ℂ → \Proc(𝕄)$. We will construct a message functor $F^{♯} ፡ \mLens(ℂ) → 𝕄$ and prove that it is the unique one satisfying $\inProc ⨾ \Proc(F^{♯}) = F$.

Let us show that such a message functor, if it were to exist, would be unique. Firstly, the image on message types is already determined to be $F^{♯}(A) = F(A)$. Secondly, the image on sessions consisting on a single morphism, $\inProc(f) ፡ [A^{∘},B^{•}]$, is determined, $F^{♯}(\inProc(f)) = F(f) ፡ [FA^{∘},FB^{•}]$. We will show now that this reasoning can be extended to all sessions:
we know that sessions of type $[X_1^{‽}, … , X_n^{‽}]$ are combs (<Ref>) of type

$$(f₀ | … | fₙ) ፡ X₁^{‽} ⊲ … ⊲ X^{‽}ₙ → \pbiobj{I}{I}.$$

This determines their image: combs can be factored as the composition, in the  of multiple sessions consisting of a single morphism (<Ref>).
Accordingly, their image, $F^{♯}(f₀ | … | fₙ)$, should be the composition, on the , of these pieces (<Ref>).

Image of a comb under the message functor.

Let us now show that we have constructed a well-defined assignment. Our construction should preserve the  equivalence relation imposed to combs. This happens, indeed, and the proof simply checks that the images of two combs,

$$(f₀ ⨾ (\id ⊗ h₀) | f₁ ⨾ (\id ⊗ h₁) | … | fₙ)  = (f₀ | (\id ⊗ h₀) ⨾ f₁ |  … | (\id ⊗ h_{n-1}) ⨾ fₙ),$$

are equal (<Ref>).

The assignment of combs to sessions preserves dinaturality.

We have constructed a well-defined assignment on sessions. Finally, we need to check that $F^{♯}$ is a message functor preserving all of the operations determined by . In the theory of combs, applying a  corresponds to a rewiring into another comb; applying the  in $𝕄$ must result in the same rewiring of the pieces forming the comb – which, as we have already shown, is precisely the image of that comb. This forces $F^{♯}$ to preserve the application of a .

We have shown that $F^{♯}$ is indeed a message functor and that it is the only possible one satisfying $\inProc ⨾ \Proc(F^{♯}) = F$.

§.§ Example: One-Time Pad, as a Message Session

Let us come back to <Ref>, where we discussed a decomposition of the one-time pad.
We now know that there is an adjunction between  and , let us use it to provide semantics to the decomposition of the one-time pad example.

The theory for the one-time pad problem can be expressed in a message theory $𝕆$ where we have a single object generator for the type of a message, $X$, and a single session generator for each one of the actors.

* $\Stage ፡ X^{∘} ⊲ X^{•} ⊲ X^{•},$

* $\Bob ፡ X^{•} ⊲ X^{∘} ⊲ X^{•},$

* $\Alice ፡ X^{∘} ⊲ X^{∘} ⊲ X^{•},$

* $\Eve ፡ X^{∘} ⊲ X^{•}.$

We will interpret these generators in the free  over the category of finite sets and stochastic maps: thanks to the adjunction, we know that, if we could interpret each one of the components presenting the category of finite sets in any , then we can interpret this whole example inside it.

We already gave an interpretation to each one of the components in terms of combs. We rewrite now the example explicitly separating each one of the parts that form it (<Ref>).

The session describing the one-time pad protocol is equal to a session where  and  communicate the message directly and  attacks a signal representing pure noise.

One-time pad, complete session.

Evaluating the session that describes the one-time pad example using the components described before, in <Ref>, obtains the following  applied to multiple combs. Evaluating the , as in <Ref>, produces the desired result.

This discussion is not restricted to the modularity of the string diagrams: it affects the modularity of the code itself.
Recall that we have a notation for sessions and ; we use it in <Ref> to write the one-time pad.

Notation for the one-time pad session.

At the same time, we have second a notation for sessions: sessions are ultimately morphisms of an , so we can use do-notation without the interchange axiom to represent them. The sending and receiving effects can be written as $(!/?)$ respectively. Lenses are tuples of morphisms, and they can be represented in do-notation using that exact characterization. The following <Ref> shows a modular implementation of the one-time pad that separates each one of the actors into a different module.

Do-notation for the one-time pad.

Which notation should we settle for? It seems that both interplay nicely together: the best way of writing a message session seems to be to write its underlying , as in <Ref>, while the best way of writing processes may be the usage of do-notation as in <Ref>, which is well-known and imposes a human-readable order on the operations.

§.§ Case Study: Causal versus Evidential Decision Theories

Leibniz's dream was to see philosophical debates reduced to mathematical calculation, to have a formal language for decision theory and an algorithm to solve any dispute.

"[...] if controversies were to arise, there would be no more need of disputation between two philosophers than between two calculators. For it would suffice for them to take their pencils in their hands and to sit down at the abacus, and say to each other (and if they so wish also to a friend called to help): calculemus (let us calculate)."

However, our modern decision theory seems far from this dream. For instance, Monty Hall's problem caused famous controversies and confident blunders of some experts <cit.> while being relatively simple to describe. It could seem that the passage from the statement to its formal encoding is more of an art than a science.

Let us try to understand one of these debates: causal versus evidential decision theory on Newcomb's problem <cit.>. We will use  to set up the scene and partial Markov categories to compute the solution.

Newcomb’s problem <cit.> is a famous decision problem
that sets apart Evidential and Causal Decision Theory. An
agent () is in front of two boxes: a transparent box filled with
1 and an opaque box (). The agent is given the choice between
taking both boxes (two-boxing, $\mathsf{T}$) and taking just the opaque
box (one-boxing, $\mathsf{O}$). However, the opaque box is controlled by
a “perfectly accurate” predictor (). The predictor placed 1000 in the
opaque box if it predicted that the agent would one-box and left it
empty otherwise. The agent knows this. Which action should
the agent choose?

Newcomb's problem: table of utilities.

At the risk of oversimplifying, most philosophers are divided in two schools <cit.>. Those that follow causal decision theory would claim that no matter what the predictor does, the lower row of the table in <Ref> contains strictly more utility; they prescribe two-boxing. Those that follow evidential decision theory claim that, because the predictor is omniscient, one-boxing is the only way of ensuring the biggest prize is on the box.

The analysis of the problem starts by dividing it into different parties: (i) the agent () must only make a choice on whether to one-box or two-box; (ii) the stage () takes the choice of the agent, the prediction of the predictor, broadcasts the choice of the agent and computes the final utility of the agent, and  (iii) the predictor () sends a prediction and, only afterwards, can see the choice of the agent. Let us call $X = \{\mathsf{O}, \mathsf{T}\}$ to the set containing one-boxing or two-boxing; we are claiming to have three elements of a : the agent,
$(\iconAgent{}) ፡ X^{•}$; the predictor, $(\iconPredictor) ፡ X^{•} ⊲ X^{∘}$; and the stage, $(\iconBoxes) ፡ X^{∘} ⊲ X^{∘} ⊲ X^{•} ⊲ X^{•}$.

Newcomb's problem: components of a message theory.

The Evidential Decision Theory Solution: Let us take as an axiom that these components are constructed out of total stochastic channels; in other words, the  we use is the free  over the Kleisli category of the subdistribution monad, $\Session(\Kleisli(\Subd))$.

We cannot assume anything about the agent, but because of the construction of out free message theory (<Ref>), it must be given by a single stochastic channel $(\iconAgent{}) ፡ I → X$.  Even without assuming anything about the predictor, because of the construction of the free message theory (<Ref>), we know that must be constructed of two parts: the one that sends the prediction, $(\iconPredictor)_1 ፡ I → M ⊗ X$, and the one that receives the choice of the agent, $(\iconPredictor)_2 ፡ M ⊗ X → I$; of the first part we know nothing, but we have postulated that we will observe it to be perfectly accurate with the prediction, meaning that the second part will fail if it is not. Thus, we deduce it must factor as in <Ref>.

Evidential reading of the predictor.

The wiring of the components is given by the statement: agent and predictor send choice and prediction to the stage, which answers giving back the choice to the predictor and computing the output (<Ref>). We then reason (i) computing the ; (ii) we analyze the agent by cases, the agent two-boxes ($\mathsf{T}$) with probability $a$ or one-boxes ($\mathsf{O}$) with probability $(1-a)$; (iii) because both cases are deterministic, they can be copied; (iv) we analyze then the predictor, it two-boxes ($\mathsf{T}$) with probability $p$ or one-boxes ($\mathsf{O}$) with probability $(1-p)$; (v) we compute according to <Ref>, canceling the incompatible equality checks; and vi assuming that the first term is just an order of magnitude larger than the second, we can bound it by $p \cdot 1000$, where we take $a = 1$: the agent should one-box.

Newcomb's problem: the solution from Evidential Decision Theory.

The Causal Decision Theory Solution: Let us assume the same components (<Ref>). The only hypothesis over which we will place suspicion is that the predictor can be “perfectly accurate” without violating causality in some way. Causal decision theory assumes that all processes are causal, or total. That means that, after receiving the news of what the agent has chosen, the predictor can do nothing: there must exist a unique total morphism $X ⊗ X → I$.

Causal reading of the predictor.

The wiring of the components is again the same, but the computation is now different: (i) we compute the ; (ii) we analyze the agent by cases, the agent two-boxes ($\mathsf{T}$) with probability $a$ or one-boxes ($\mathsf{O}$) with probability $(1-a)$; (iii) we analyze in the same way the predictor; (iv) we compute according to <Ref>, canceling the incompatible equality checks; and (v) we bound everything by the case where $a = 0$: this time, to maximize utility, the agent must two-box.

Newcomb's problem: the solution from Causal Decision Theory.

Was this formal analysis better than a pure discussion? We can now claim that the advantage is that the computations go from a starting diagram that represents our reading of the problem to a utility that we can maximize. We have turned most of the problem into a problem of computation: not only looking at the table of utilities (<Ref>) but at the whole statement of the problem. Of course, our formalization does not solve the debate on Newcomb's paradox, but at least it moves the controversy to a more fundamental point: are we fine with using the action of the agent to reason acausally about the predictor? The algebra of partial Markov categories provides a mathematical framework where it makes sense to assume so; the algebra of  takes care of the rest of the discussion.

§.§ Bibliography

The idea of using send/receive effects for encoding sessions is not new.
Message passing can be also seen as a core component of game semantics, which has a vast literature <cit.>. Game semantics has the ambition to provide the mathematical structures that describe coordination between distributed agents, starting from a duality between the Player's moves and the Opponent's moves; one of its achievements is to provide syntax-independent semantics for different extensions of PCF <cit.>, including one with global state <cit.>.

Game semantics and session types <cit.> have been called “two sides of the same coin” <cit.>.
Orchard and Yoshida <cit.> discuss two mutual embeddings between an effectful $\lambda$-calculus (PCF) and a session $\pi$-calculus; further work also implemented the corresponding do-notation <cit.>. In our framework, this correspondence occurs between  and ; and thus between do-notation and .

Particularly relevant is Melliès' categorical approach to game semantics in the form of template games <cit.>. The crucial difference between the present proposal and Melliès' line of work is that it starts from labelled transition systems as the basic notion. Melliès introduces asynchronous graphs – graphs with a set of commuting squares – and many of the same ingredients that we use here. Asynchronous graphs explain shuffles, polarization, and a failure of interchange in the form of a Grey tensor product <cit.>. We would be interested to compare our approach to message passing with the framework of template games, and especially the points where they diverge: we land on  while template games are based on Girard's linear logic <cit.>.

Finally, Newcomb's problem (or paradox) was first stated by Nozick <cit.>. Evidential decision theory is defended in the work of Ahmad <cit.>; both Everitt, Leike and Hutter <cit.>, and Yudkowsky and Soares <cit.> have formalized comparisons of evidential decision theory, causal decision theory, and further variants.

CHAPTER: CONCLUSIONS AND FURTHER WORK

§ CONCLUSIONS

§.§ Monoidal Context Theory

We have universally characterized the  of  (<Ref>) as a free normalization of the cofree  on top of a . The interpretation of this result is relevant: the splice-contour adjunction (<cit.>, <Ref>) relates each category to its cofree  of incomplete terms; in the same way, we have constructed a monoidal splice-contour adjunction relating each  to its cofree  of incomplete processes. The category underlying this universal  is familiar: it is the category of .

have gained recent popularity in applications of category theory, apart from their classical counterparts in database theory <cit.>: they have spawned applications in bidirectional transformations <cit.> but also in functional programming <cit.>, open games <cit.>, polynomial functors <cit.> and quantum combs <cit.>. Moreover, a different  structure for lenses had been already studied in the past by Pastro and Street <cit.>. Apart from lenses, incomplete processes have appeared implicitly multiple times in recent literature. Kissinger and Uijlen <cit.> describe higher-order quantum processes using contexts with holes in compact closed monoidal categories. Ghani, Hedges, Winschel and Zahn <cit.> describe economic game theory in terms of lenses and incomplete processes in cartesian monoidal categories. Bonchi, Piedeleu,  and Zanasi <cit.> study contextual equivalence in their monoidal category of affine signal flow graphs. Di Lavore, de Felice and Román <cit.> define monoidal streams by iterating monoidal context coalgebraically.
This situation prompted a question: why are lenses so prevalent? why do they appear in seemingly unrelated applications?  We can now claim a conceptual answer with a mathematical justification. Lenses are the universal algebra for decomposing morphisms in process theories. The recent applications of lenses all describe incomplete processes.

Incomplete processes have two uses: on the one hand, they track the dependencies between monoidal processes; on the other hand, they allow us to split the multiple agents of a multi-party process. The former is quite useful in itself:  provide two different tensors – a sequential, $(⊲)$, and a parallel one $(⊗)$ – that can track dependencies between different processes (as we saw in <Ref>). Signalling and non-signalling conditions are important to the study of quantum theories, and recent work by Wilson and Chiribella <cit.> and Hefford and Kissinger <cit.> has studied signalling using structures close to ; we hope that the universal characterization of lenses as cofree  may help extracting the exact structure needed for these physical frameworks. Even forgetting about dependencies explicitly, the theory of monoidal contexts allows us to pursue branches of computer science that were classically restricted to 1-dimensional syntaxes: the recent work of Eanrshaw and Sobocinski <cit.> studies monoidal regular languages as the natural monoidal analogue of the classical notion of regular language.

However, it is the second application of incomplete processes the one that this author found more surprising: we can now separate the different agents of a multi-party process in an arbitrary . Message passing was not the main goal of this thesis, but developing it has brought interesting connections to game semantics.

§.§ Monoidal Message Passing

have two operations: sequential composition $(⨾)$ and parallel composition $(⊗)$. Naively, we would think then that there are two ways of decomposing monoidal processes: sequentially and in parallel. This is not false, and for many applications this may be the simpler way of dealing with this; after all, glueing sequentially and in parallel is the only thing we need to separate a string diagram in its atomic parts. However, this misses the rich algebra of incomplete morphisms and their compositions:  can be composed according to any , and that is the algebra that we are implicitly using when we cut a string diagram into pieces that do not necessarily follow the sequential and parallel divisions.
We can now argue that the algebra of message passing for process theories is that of .  try to be a minimalistic axiomatization of what it means to communicate different processes that send and receive messages: we have argued for these axioms in <Ref>, in a way that should appeal any reader not familiar with the categorical framework behind them. Their combinatorial characterization in terms of  only makes them more concrete.

We have developed a theory of context on top of  and we have used it to develop a canonical theory of message passing in .
We have argued that this a fundamental structure for concurrency, and we have characterized it universally; however, we could still argue that it does not address the problem posed by Abramsky of finding the fundamental structures of concurrency <cit.>. The main limitation of this framework is that it does not provide most of the features that we expect from fully-fledged session types: how can we model choice, or synchrony <cit.>? how can we model iteration, feedback, or other common programming constructs <cit.>?
Minimalism, however, may be a good thing to separate these concerns from the fundamental structure: if we want to model choice, we can do so using distributive categories <cit.>, or linear actegories <cit.>; if we want feedback and iteration, we can recall traced categories <cit.>, categories with feedback <cit.>, and notions of monoidal automata <cit.>. Precisely because our framework is minimal, it seems that it is robust enough to support these additions; we will be interested in constructing models of game semantics in further work.

§.§ Future Work

Monoidal game semantics was not the original goal of this project but it became its most promising avenue; last section gives us a recipe to construct a session do-notation calculus on top of any , which would include stochastic, non-deterministic and partial variants of a multi-party do-notation calculus. Levy, Power and Thielecke <cit.> discuss the correspondence between  and call-by-value languages; we would be interested in extending this correspondence into message passing <cit.>. Once there, it seems plausible that we can connect this idea to the literature on game semantics for fully-fledged programming semantics <cit.>. Specifically, we would like to construct a model of probabilistic programming allowing for message passing, choice and iteration; multiple developments in categorical probability (such as quasiborel spaces <cit.> or Markov categories <cit.>) make this possible.

The existence of a vast literature on message passing in terms of linear actions <cit.> makes it particularly important to understand exactly how  and linear logic relate. We conjecture that  also form isomix linearly distributive categories <cit.>, and this may be a categorical justification behind this connection.

For conciseness, we have not discussed approaches to iteration in . Joint work of this author with Di Lavore and de Felice <cit.> has shown that it is possible to reason coinductively with automata in , using precisely  to describe incomplete processes. It seems plausible then, that mixing coinduction with message passing allows us to talk about networks of stochastic iterative processes: these have remarkable applications in scientific modelling, where we can write causal networks of stochastic processes in which unknown components are approximated stochastically.

CHAPTER: APPENDIX

§ COHERENCE DIAGRAMS FOR A DUOIDAL CATEGORY

((A ◁ B) ⊗ (C ◁ D)) ⊗ (E ◁ F)
α [swap]ψ₂ ⊗ id
(A ◁ B) ⊗ ((C ◁ D) ⊗ (E ◁ F))
id ⊗ ψ₂

((A ⊗ C) ◁ (B ⊗ D)) ⊗ (E ◁ F)
(A ◁ B) ⊗ ((C ⊗ E) ◁ (D ⊗ F))

((A ⊗ C) ⊗ E) ◁ ((B ⊗ D) ⊗ F)
α ◁ α
(A ⊗ (C ⊗ E)) ◁ (B ⊗ (D ⊗ F))

((A ◁ B) ◁ C) ⊗ ((D ◁ E) ◁ F)
β⊗ β [swap]ψ₂
(A ◁ (B ◁ C)) ⊗ (D ◁ (E ◁ F))

((A ◁ B) ⊗ (D ◁ E)) ◁ (C ⊗ F)
[swap]ψ₂ ⊗ id
(A ⊗ D) ◁ ((B ◁ C) ⊗ (E ◁ F))
id ⊗ ψ₂

((A ⊗ D) ◁ (B ⊗ E)) ◁ (C ⊗ F)
(A ⊗ D) ◁ ((B ⊗ E) ◁ (C ⊗ F))

Coherence diagrams for associativity of a duoidal category.

I ⊗ (A ◁ B)
ψ₀ ⊗ id [swap]λ
(I ◁ I) ⊗ (A ◁ B)

A ◁ B

(I ⊗ A) ◁ (I ⊗ B)
λ◁ λ

(A ◁ B) ⊗ I
ψ₀ ⊗ id [swap]ρ
(A ◁ B) ⊗ (I ◁ I)

A ◁ B

(A ⊗ I) ◁ (B ⊗ I)
ρ◁ ρ

Coherence diagrams for $⊗$-unitality of a duoidal category.

N ◁ (A ⊗ B)
(N ⊗ N) ◁ (A ⊗ B)
[swap]φ_2 ◁ id ψ₂

A ⊗ B

(N ◁ A) ⊗ (N ◁ B)
κ ⊗ κ

(A ⊗ B) ◁ N
(A ⊗ B)  ◁ (N ⊗ N)
[swap]id ◁ φ_2 ψ₂

A ⊗ B

(A ◁ N) ⊗ (B ◁ N)
ν ⊗ ν

Coherence diagrams for $◁$-unitality of a duoidal category.

(N ⊗ N) ⊗ N
rrα [swap]φ_2 ⊗ id
N ⊗ (N ⊗ N)
id ⊗ φ_2

N ⊗ N

N ⊗ N

I ◁ I
[swap]ψ_0 ⊗ id
[swap]ψ_0 ψ_0
I ◁ I
id ⊗ ψ_0

(I ◁ I) ◁ I
I ◁ (I ◁ I)

Associativity and coassociativity for $N$ and $I$ in a duoidal category.

N ⊗ I
ρ [swap]id ⊗ φ_0

N ⊗ N

I ⊗ N
λ [swap]φ_0 ⊗ id

N ⊗ N

I ◁ N
id ⊗ φ_0 [swap]ν
I ◁ I

N ◁ I
id ⊗ φ_0 [swap]κ
I ◁ I

Unitality and counitality for $N$ and $I$ in a duoidal category.

§ POLYCATEGORIES

This extra section repeats the splice-contour adjunction for . It is a detour from the main text; and it is not necessary for its development: this does not seem to be the direction we want to follow to study context in categories or . It is, however, another proof of the resilience of the splice-contour adjunction: the duality between a category and its opposite induces a pseudofrobenius algebra on the monoidal bicategory of profunctors.

§.§ Polycategories

A  is like a category where every morphism has both a list of inputs and a list of outputs <cit.>. This does not mean that its inputs and outpuss start forming a monoid, as in strict monoidal categories; morphisms really have different multiple inputs and outputs, and we need to choose a single one to compose along it.
A polycategory, $ℙ$, contains a set of objects, $ℙ_{obj}$, as categories and multicategories; but instead of a set of morphisms, it will have a set of polymorphisms,

$$ℙ(X₁,…,Xₙ; Y₁,…, Yₘ),$$

for each two lists of objects $X₁, …, Xₙ , Y₀, …, Yₘ ∈ ℙ_{obj}$. As in linear logic, we denote both sides of a derivation by two metavariables, $Γ = X₁, …, Xₙ$ and $Δ = Y₀, …, Yₘ$, and write $ℙ(Γ; Δ)$ for the set of polymorphisms.

A polycategory $ℙ$ is a collection of objects, $ℙ_{obj}$, together with a collection of polymorphisms, $ℙ(X₀,\dots,Xₙ; Y₀,\dots,Yₘ)$, for each two lists of objects $X₀,\dots,Xₙ \in ℙ$ and $Y₀,\dots,Yₘ \in ℙ$. For each object $X \in ℙ_{obj}$, there must be an identity, $\mathrm{id}_X \in ℙ_{obj}(X;X)$; and for each pair of composable maps,

\begin{align*}
& f \in ℙ(\Gamma ; \Delta₁, X, \Delta₂) \mbox{ and } g \in ℙ(\Gamma₁,X,\Gamma₂; \Delta),\\
& \qquad\mbox{ where either }
\Delta₁\mbox{ or }\Gamma₁,\mbox{ and either }\Delta₂\mbox{ or }\Gamma₂,\mbox{ are empty,}
\end{align*}

there must be a composite polymorphism $f ⨾_X g \in ℙ(\Gamma₁,\Gamma,\Gamma₂; \Delta₁,\Delta,\Delta₂)$.
This means that there are four possible types of composition (<Ref>), and they yield the same polymorphism whenever they overlap.

[x=0.75pt,y=0.75pt,yscale=-1,xscale=1,line width=1pt]

(265.06,109.94) – (265,80) ;

(270,110) .. controls (269.78,124.33) and (274.89,119.89) .. (275,135) ;

(260,110) .. controls (259.78,124.33) and (254.89,119.89) .. (255,135) ;

(265,105) .. controls (264.78,90.67) and (279.89,95.11) .. (280,80) ;

(265,105) .. controls (264.78,90.67) and (249.89,95.11) .. (250,80) ;

(90,115) .. controls (90.22,126.47) and (85.11,122.91) .. (85,135) ;

(100,115) .. controls (100.22,126.47) and (105.11,122.91) .. (105,135) ;

(95.03,104.97) .. controls (80.56,99.67) and (95.22,84.78) .. (95,65) ;

(70,75) .. controls (81,81) and (70.11,89.89) .. (70,110) ;

(65,70) .. controls (65.22,55.67) and (60.11,60.11) .. (60,45) ;

(75,70) .. controls (75.22,55.67) and (80.11,60.11) .. (80,45) ;

(70,70) – (60,75) ;

(105.03,104.97) – (95.03,109.97) ;

(94.94,109.94) – (85,105) ;

[fill=rgb, 255:red, 255; green, 255; blue, 255   ,fill opacity=1 ] (104.88,109.94) .. controls (104.88,104.45) and (100.43,100) .. (94.94,100) .. controls (89.45,100) and (85,104.45) .. (85,109.94) .. controls (85,115.43) and (89.45,119.88) .. (94.94,119.88) .. controls (100.43,119.88) and (104.88,115.43) .. (104.88,109.94) – cycle ;

(80,75) – (70,70) ;

[fill=rgb, 255:red, 255; green, 255; blue, 255   ,fill opacity=1 ] (79.88,70.06) .. controls (79.88,75.55) and (75.43,80) .. (69.94,80) .. controls (64.45,80) and (60,75.55) .. (60,70.06) .. controls (60,64.57) and (64.45,60.12) .. (69.94,60.12) .. controls (75.43,60.12) and (79.88,64.57) .. (79.88,70.06) – cycle ;

(80,75) .. controls (89.73,80.09) and (74.82,100.27) .. (85,105) ;

(59.97,75.03) .. controls (49.73,80.09) and (55,85.36) .. (55,105) ;

(55,135) – (55,105) ;

(110,75) – (110,45) ;

(105.03,104.97) .. controls (115.27,99.91) and (110,94.64) .. (110,75) ;

[draw opacity=0] (125,40) – (50,40) – (50,140) – (125,140) – cycle ;

(95,65) – (95,45) ;

(70,135) – (70,110) ;

[draw opacity=0] (55,135) – (70,135) – (70,150) – (55,150) – cycle ;

[draw opacity=0] (85,135) – (105,135) – (105,150) – (85,150) – cycle ;

[draw opacity=0] (95,30) – (110,30) – (110,45) – (95,45) – cycle ;

[draw opacity=0] (60,30) – (80,30) – (80,45) – (60,45) – cycle ;

(165,115) .. controls (164.78,126.47) and (169.89,122.91) .. (170,135) ;

(155,115) .. controls (154.78,126.47) and (149.89,122.91) .. (150,135) ;

(159.97,104.97) .. controls (174.44,99.67) and (159.78,84.78) .. (160,65) ;

(185,75) .. controls (174,81) and (184.89,89.89) .. (185,110) ;

(190,70) .. controls (189.78,55.67) and (194.89,60.11) .. (195,45) ;

(180,70) .. controls (179.78,55.67) and (174.89,60.11) .. (175,45) ;

(185,70) – (195,75) ;

(149.97,104.97) – (159.97,109.97) ;

(160.06,109.94) – (170,105) ;

[fill=rgb, 255:red, 255; green, 255; blue, 255   ,fill opacity=1 ] (150.12,109.94) .. controls (150.12,104.45) and (154.57,100) .. (160.06,100) .. controls (165.55,100) and (170,104.45) .. (170,109.94) .. controls (170,115.43) and (165.55,119.88) .. (160.06,119.88) .. controls (154.57,119.88) and (150.12,115.43) .. (150.12,109.94) – cycle ;

(175,75) – (185,70) ;

[fill=rgb, 255:red, 255; green, 255; blue, 255   ,fill opacity=1 ] (175.12,70.06) .. controls (175.12,75.55) and (179.57,80) .. (185.06,80) .. controls (190.55,80) and (195,75.55) .. (195,70.06) .. controls (195,64.57) and (190.55,60.12) .. (185.06,60.12) .. controls (179.57,60.12) and (175.12,64.57) .. (175.12,70.06) – cycle ;

(175,75) .. controls (165.27,80.09) and (180.18,100.27) .. (170,105) ;

(195.03,75.03) .. controls (205.27,80.09) and (200,85.36) .. (200,105) ;

(200,135) – (200,105) ;

(145,75) – (145,45) ;

(149.97,104.97) .. controls (139.73,99.91) and (145,94.64) .. (145,75) ;

(160,65) – (160,45) ;

(185,135) – (185,110) ;

[draw opacity=0] (145,30) – (160,30) – (160,45) – (145,45) – cycle ;

[draw opacity=0] (175,30) – (195,30) – (195,45) – (175,45) – cycle ;

[draw opacity=0] (150,135) – (170,135) – (170,150) – (150,150) – cycle ;

[draw opacity=0] (185,135) – (200,135) – (200,150) – (185,150) – cycle ;

(270,70) .. controls (269.78,55.67) and (274.89,60.11) .. (275,45) ;

(260,70) .. controls (259.78,55.67) and (254.89,60.11) .. (255,45) ;

[fill=rgb, 255:red, 255; green, 255; blue, 255   ,fill opacity=1 ] (255.12,70.06) .. controls (255.12,75.55) and (259.57,80) .. (265.06,80) .. controls (270.55,80) and (275,75.55) .. (275,70.06) .. controls (275,64.57) and (270.55,60.12) .. (265.06,60.12) .. controls (259.57,60.12) and (255.12,64.57) .. (255.12,70.06) – cycle ;

(270,105) .. controls (269.78,90.67) and (299.89,95.11) .. (300,80) ;

(260,105) .. controls (259.78,90.67) and (229.89,95.11) .. (230,80) ;

[fill=rgb, 255:red, 255; green, 255; blue, 255   ,fill opacity=1 ] (255.12,109.94) .. controls (255.12,115.43) and (259.57,119.88) .. (265.06,119.88) .. controls (270.55,119.88) and (275,115.43) .. (275,109.94) .. controls (275,104.45) and (270.55,100) .. (265.06,100) .. controls (259.57,100) and (255.12,104.45) .. (255.12,109.94) – cycle ;

(230,80) – (230,45) ;

(250,80) – (250,45) ;

(280,80) – (280,45) ;

(300,80) – (300,45) ;

[draw opacity=0] (255,30) – (275,30) – (275,45) – (255,45) – cycle ;

[draw opacity=0] (280,30) – (300,30) – (300,45) – (280,45) – cycle ;

[draw opacity=0] (230,29) – (250,29) – (250,44) – (230,44) – cycle ;

[draw opacity=0] (255,135) – (275,135) – (275,150) – (255,150) – cycle ;

(360.06,70.06) – (360,100) ;

(365,70) .. controls (364.78,55.67) and (369.89,60.11) .. (370,45) ;

(355,70) .. controls (354.78,55.67) and (349.89,60.11) .. (350,45) ;

(360,75) .. controls (359.78,89.33) and (374.89,84.89) .. (375,100) ;

(360,75) .. controls (359.78,89.33) and (344.89,84.89) .. (345,100) ;

(365,110) .. controls (364.78,124.33) and (369.89,119.89) .. (370,135) ;

(355,110) .. controls (354.78,124.33) and (349.89,119.89) .. (350,135) ;

[fill=rgb, 255:red, 255; green, 255; blue, 255   ,fill opacity=1 ] (350.12,109.94) .. controls (350.12,104.45) and (354.57,100) .. (360.06,100) .. controls (365.55,100) and (370,104.45) .. (370,109.94) .. controls (370,115.43) and (365.55,119.88) .. (360.06,119.88) .. controls (354.57,119.88) and (350.12,115.43) .. (350.12,109.94) – cycle ;

(365,75) .. controls (364.78,89.33) and (394.89,84.89) .. (395,100) ;

(355,75) .. controls (354.78,89.33) and (324.89,84.89) .. (325,100) ;

[fill=rgb, 255:red, 255; green, 255; blue, 255   ,fill opacity=1 ] (350.12,70.06) .. controls (350.12,64.57) and (354.57,60.12) .. (360.06,60.12) .. controls (365.55,60.12) and (370,64.57) .. (370,70.06) .. controls (370,75.55) and (365.55,80) .. (360.06,80) .. controls (354.57,80) and (350.12,75.55) .. (350.12,70.06) – cycle ;

(325,100) – (325,135) ;

(345,100) – (345,135) ;

(375,100) – (375,135) ;

(395,100) – (395,135) ;

[draw opacity=0] (350,30) – (370,30) – (370,45) – (350,45) – cycle ;

[draw opacity=0] (325,136) – (345,136) – (345,151) – (325,151) – cycle ;

[draw opacity=0] (350,135) – (370,135) – (370,150) – (350,150) – cycle ;

[draw opacity=0] (375,136) – (395,136) – (395,151) – (375,151) – cycle ;

(69.91,70.14) node  [font=]  $f$;

(95.03,109.97) node  [font=]  $g$;

(62.5,142.5) node  [font=]  $\Delta _{1}$;

(95,142.5) node  [font=]  $\Delta $;

(102.5,37.5) node  [font=]  $\Gamma _{2}$;

(70,37.5) node  [font=]  $\Gamma $;

(185.06,70.06) node  [font=]  $f$;

(159.97,109.97) node  [font=]  $g$;

(152.5,37.5) node  [font=]  $\Gamma _{1}$;

(185,37.5) node  [font=]  $\Gamma $;

(160,142.5) node  [font=]  $\Delta $;

(192.5,142.5) node  [font=]  $\Delta _{2}$;

(265.06,70.06) node  [font=]  $f$;

(265.06,109.94) node  [font=]  $g$;

(265,37.5) node  [font=]  $\Gamma $;

(290,37.5) node  [font=]  $\Gamma _{2}$;

(240,36.5) node  [font=]  $\Gamma _{1}$;

(265,142.5) node  [font=]  $\Delta $;

(360.06,109.94) node  [font=]  $g$;

(360.06,70.06) node  [font=]  $f$;

(358.5,37.5) node  [font=]  $\Gamma $;

(335,143.5) node  [font=]  $\Delta _{1}$;

(360,142.5) node  [font=]  $\Delta $;

(385,143.5) node  [font=]  $\Delta _{2}$;

Four planar polycategorical compositions.

Moreover, polycategories must satisfy the following two unitality axioms, $f ⨾_X \mathrm{id}_X = f$ and $\mathrm{id}_X ⨾_X f = f$; two associativity axioms, $f ⨾_X (g ⨾_Y h) = (f ⨾_X g) ⨾_Y h$ and $f ⨾_X (g ⨾_Y h) = g ⨾_Y (f ⨾_X h)$; and an interchange axiom, $(f ⨾_A g) ⨾_B h = (f ⨾_B h) ⨾_A g$; whenever any of these is formally well-typed.

Asking for an identity on each object, $\mathrm{id}_X \in ℙ(X;X)$, is different from asking for an identity on each list of objects,
$$\mathrm{id}_{X₀,\dots,Xₙ} \in ℙ(X₀,\dots,Xₙ;X₀,\dots,Xₙ).$$
The latter gives rise to isomix categories <cit.> and we will not discuss it here.

A polyfunctional relation, $R \in \mathbf{MultiFun}(A₁,\dots, Aₙ; B₁,\dots, Bₘ)$, is a relation $R \colon A₁ × \dots × Aₙ → B₁ × \dots × Bₘ$ together with representing functions that, given an element of the relation missing exactly one element, return the element missing. Explicitly, there exist two families of functions,

\begin{align*}
& fⱼ ፡ A₁ × \dots × A_n × B₀ × \overset{\cancel{B_j}}\dots × B_m → B_j
\quad\mbox{ and } \\
& g_i \colon A₁ \times \overset{\cancel{A_i}}\dots \times Aₙ × B_0 × \dots × B_m → Aᵢ,
\end{align*}

such that $R(a₁,…,bₘ)$ if and only if $fⱼ(a₁,…,bₘ) = bⱼ$ and if and only if $g_i(a₁,…,bₘ) = aᵢ$ for each two indices $i$ and $j$. Polyfunctional relations form a  with relational composition.

A $(1,1)$-polyfunctional relation is a pair of inverse functions. A (2,1) or (1,2)-polyfunctional relation is a triple functions $f₀ ፡ A₁ × A₂ → A₀$, $f₁ ፡ A₂ × A₀ → A₁$ and $f₂ ፡ A₀ × A₁ → A₂$ such that
$f₁(a_1,a_2) = a_0$ if and only if
$f_1(a_2,a_0) = a_1$ and if and only if
$f_2(a_0,a_1) = a_2$.
Polyfunctional relations are a decategorification of the multivariable adjunctions in the work of Shulman <cit.>.

§.§ The Category of Polycategories

Analogously to the categorical and multicategorical case, the theory of  and polynatural transformations is synthetised in the 2-category $\mathbf{PolyCat}$ of polycategories, polyfunctors and polynatural transformations.

A polyfunctor, $F \colon ℙ → ℚ$, between two  $ℙ$ and $ℚ$, is an assignment on objects, $F_{obj} \colon ℙ_{obj} → ℚ_{obj}$ together with an assignment on polymorphisms

$$F_{n,m} \colon ℙ(X₀, \dots, Xₙ; Y₀, \dots, Yₘ) → ℚ(F_{obj}X₀, \dots, F_{obj}Xₙ; F_{obj}Y₀, \dots, F_{obj}Yₘ).$$

This assignment must be functorial, in that $F(f ⨾_{X_i} g) = F(f) ⨾_{X_i} F(g)$ and that $F(\mathrm{id}_X) = \mathrm{id}_{FX}$, whenever these are formally well-typed.

A polynatural transformation $θ ፡ F → G$ between two  $F, G ፡ ℙ → ℚ$ is given by a family of polymorphisms $θ_X ∈ ℚ(FX; GX)$ such that, for each polymorphism $f ∈ ℙ(X₁, …, Xₙ; Y₁, …, Yₘ)$, the following naturality condition holds

$$θ_{X₁} ⨾ … ⨾ θ_{Xₙ} ⨾ G(f) = F(f) ⨾ θ_{Y₁} ⨾ … ⨾ θ_{Yₘ}.$$

Polyfunctors between polycategories form a category, $\mathbf{PolyCat}$.
This is moreover a 2-category with polynatural transformations.

In the same sense that a multifunctor from the terminal  picks a monoid, a polyfunctor from the terminal  should pick a polyoid – instead, we call these Frobenius monoids.

§.§ Polycategorical Contour

Let $ℙ$ be a . Its contour, $\Contour{ℙ}$, is the category presented by the following generators and equations:

* two polarized objects, $Xˡ$ and $Xʳ$, for each object $X ∈ ℙ_{obj}$;

* for each polymorphism, $f ∈ ℙ(X₁,…,Xₙ ; Y₁,…,Yₘ)$, the following generators,

\begin{align*}
& fʳ_1 ፡ Xʳ_1 → Xˡ_2, \quad …, \quad fʳ_{n-1} ፡ Xʳ_{n-1} → Xˡ_n, \quad fᵈ ፡ Xʳ_n → Y^r_m, \\
& fˡ_1 ፡ Yˡ_2 → Yʳ_1, \quad …, \quad fˡ_{m-1} ፡ Yˡ_m → Yʳ_{m-1}, \quad fᵘ ፡ Yˡ_1 → Xˡ_1,
\end{align*}

having instead $fᵘ ፡ Yˡ_1 → Yʳ_m$ when $n = 0$, having instead $fᵈ ፡ Xʳ_n → Xˡ_1$ when $m = 0$, and using no generators for $(0,0)$-polymorphisms;

to which we impose equations 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₁,…,Xₙ;Y₁,…,Yₘ)$ and each $g ∈ ℙ(Z₁,…,Zₚ;Q₁,…,Q_q)$ such that $Yₘ = U₁$, the contour of the composition along $Yₘ = U₁$ is defined by the following eight cases

\begin{align*}
& (f ⨾_{Xᵢ} g)ᵘ = fᵘ;
&& (f ⨾_{Xᵢ} g)ʳ_i = f^r_i,\mbox{ for } i = 1,…,n-1; \\
& (f ⨾_{Yₘ} g)ʳ_n = fᵈ ⨾ gʳ_1;
&& (f ⨾_{Yₘ} g)ʳ_j = gʳ_{j-n+1},\mbox{ for } j = n+1, …, n+p-2; \\
& (f ⨾_{Yₘ} g)ᵈ = gᵈ;
&& (f ⨾_{Yₘ} g)ˡ_i = fˡ_i,\mbox{ for } i = 1,…,m-2; \\
& (f ⨾_{Yₘ} g)ᵈ_{m-1} = gᵘ ⨾ fˡ_{m-1};
&& (f ⨾_{Yₘ} g)ᵈ_{j} = gˡ_{j-m+1},\mbox{ for } j = m+1,…,m+q-2;
\end{align*}

and similar conditions for the rest of the compositions. These equations are depicted in <Ref>.

every picture/.style=line width=0.95pt

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (85,85) – (98,85) ;
[shift=(100,85), rotate = 180] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (72.92,85.22) .. controls (60.44,87.7) and (60.89,110) .. (75,110) ;
[shift=(75,85), rotate = 178.88] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0] (110,75) – (125,75) – (125,90) – (110,90) – cycle ;

[draw opacity=0] (85,70) – (100,70) – (100,85) – (85,85) – cycle ;

(80,105) – (80,125) ;

(105,105) – (105,125) ;

(130,105) – (130,125) ;

(155,105) – (155,125) ;

(80,70) – (80,90) ;

(105,70) – (105,90) ;

(130,70) – (130,90) ;

(155,70) – (155,90) ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (135,85) – (148,85) ;
[shift=(150,85), rotate = 180] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0] (135,70) – (150,70) – (150,85) – (135,85) – cycle ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (100,110) – (87,110) ;
[shift=(85,110), rotate = 360] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0] (110,105) – (125,105) – (125,120) – (110,120) – cycle ;

[draw opacity=0] (45,90) – (65,90) – (65,105) – (45,105) – cycle ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (150,110) – (137,110) ;
[shift=(135,110), rotate = 360] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0] (135,110) – (150,110) – (150,125) – (135,125) – cycle ;

(75,93) .. controls (75,91.34) and (76.34,90) .. (78,90) – (157,90) .. controls (158.66,90) and (160,91.34) .. (160,93) – (160,102) .. controls (160,103.66) and (158.66,105) .. (157,105) – (78,105) .. controls (76.34,105) and (75,103.66) .. (75,102) – cycle ;

[draw opacity=0] (240,55) – (265,55) – (265,70) – (240,70) – cycle ;

(240,85) – (240,145) ;

(265,85) – (265,145) ;

(240,50) – (240,70) ;

(290,50) – (290,70) ;

(235,73) .. controls (235,71.34) and (236.34,70) .. (238,70) – (292,70) .. controls (293.66,70) and (295,71.34) .. (295,73) – (295,82) .. controls (295,83.66) and (293.66,85) .. (292,85) – (238,85) .. controls (236.34,85) and (235,83.66) .. (235,82) – cycle ;

(295,113) .. controls (295,111.34) and (296.34,110) .. (298,110) – (352,110) .. controls (353.66,110) and (355,111.34) .. (355,113) – (355,122) .. controls (355,123.66) and (353.66,125) .. (352,125) – (298,125) .. controls (296.34,125) and (295,123.66) .. (295,122) – cycle ;

(290,85) .. controls (290.67,100.83) and (300,95.17) .. (300,110) ;

(325,50) – (325,110) ;

(350,50) – (350,110) ;

(300,125) – (300,145) ;

(350,125) – (350,145) ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (290,100) .. controls (274.67,100.17) and (279,130.17) .. (295,130) ;

(265,50) – (265,70) ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (270,65) – (283,65) ;
[shift=(285,65), rotate = 180] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (290,100) .. controls (280.13,99.86) and (285.52,90.93) .. (271.82,90.06) ;
[shift=(270,90), rotate = 0.6] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (300,95) .. controls (315.33,94.83) and (311,64.83) .. (295,65) ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (300,95) .. controls (309.87,95.14) and (304.48,104.07) .. (318.18,104.94) ;
[shift=(320,105), rotate = 180.6] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0] (240,85) – (265,85) – (265,100) – (240,100) – cycle ;

(325,125) – (325,145) ;

[draw opacity=0] (325,95) – (350,95) – (350,110) – (325,110) – cycle ;

[draw opacity=0] (325,125) – (350,125) – (350,140) – (325,140) – cycle ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (320,130) – (307,130) ;
[shift=(305,130), rotate = 360] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (232.92,65.22) .. controls (220.44,67.7) and (220.89,90) .. (235,90) ;
[shift=(235,65), rotate = 178.88] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (160,85) .. controls (173.92,85.27) and (174.8,107.83) .. (161.91,109.85) ;
[shift=(160,110), rotate = 360] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0] (170,90) – (190,90) – (190,105) – (170,105) – cycle ;

(425,50) – (425,145) ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (431.04,85) .. controls (444.95,85.27) and (445.84,107.83) .. (432.95,109.85) ;
[shift=(431.04,110), rotate = 360] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (417.92,85.22) .. controls (405.44,87.7) and (405.89,110) .. (420,110) ;
[shift=(420,85), rotate = 178.88] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0] (185,85) – (205,85) – (205,110) – (185,110) – cycle ;

[draw opacity=0] (370,85) – (390,85) – (390,110) – (370,110) – cycle ;

[draw opacity=0] (400,75) – (450,75) – (450,120) – (400,120) – cycle ;

[color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ]   (355,105) .. controls (368.92,105.27) and (369.8,127.83) .. (356.91,129.85) ;
[shift=(355,130), rotate = 360] [color=rgb, 255:red, 94; green, 129; blue, 172   ,draw opacity=1 ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0] (390,90) – (410,90) – (410,105) – (390,105) – cycle ;

[draw opacity=0] (440,90) – (460,90) – (460,105) – (440,105) – cycle ;

[draw opacity=0] (460,85) – (480,85) – (480,110) – (460,110) – cycle ;

[draw opacity=0] (135,70) – (150,70) – (150,85) – (135,85) – cycle ;

[draw opacity=0] (170,90) – (185,90) – (185,105) – (170,105) – cycle ;

[draw opacity=0] (135,110) – (150,110) – (150,125) – (135,125) – cycle ;

[draw opacity=0] (85,110) – (100,110) – (100,125) – (85,125) – cycle ;

[draw opacity=0] (85,110) – (100,110) – (100,125) – (85,125) – cycle ;

[draw opacity=0] (205,70) – (225,70) – (225,85) – (205,85) – cycle ;

[draw opacity=0] (365,110) – (385,110) – (385,125) – (365,125) – cycle ;

[draw opacity=0] (365,110) – (380,110) – (380,125) – (365,125) – cycle ;

[draw opacity=0] (270,50) – (285,50) – (285,65) – (270,65) – cycle ;

[draw opacity=0] (270,50) – (285,50) – (285,65) – (270,65) – cycle ;

[draw opacity=0] (305,130) – (320,130) – (320,145) – (305,145) – cycle ;

[draw opacity=0] (305,130) – (320,130) – (320,145) – (305,145) – cycle ;

(117.5,97.5) node    $f$;

(117.5,82.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $\dotsc $;

(92.5,73.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $f_{1}^{r}$;

(117.5,112.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $\dotsc $;

(55,97.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $f^{u}$;

(265,77.5) node    $f$;

(252.5,62.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $\dotsc $;

(325,117.5) node    $g$;

(252.5,92.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $\dotsc $;

(337.5,102.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $\dotsc $;

(337.5,132.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $\dotsc $;

(195,97.5) node    $;$;

(380,97.5) node    $;$;

(400,97.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $id$;

(450,97.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $id$;

(470,97.5) node    $;$;

(142.5,73.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $f_{n-1}^{r}$;

(180.5,97.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $f^{d}$;

(142.5,120.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $f_{m-1}^{\ell}$;

(92.5,120.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $f_{1}^{\ell}$;

(215,77.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $f^{u}$;

(374.5,117.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $f^{d}$;

(277.5,53.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $f_{n-1}^{r}$;

(312.5,140.5) node  [font=,color=rgb, 255:red, 94; green, 129; blue, 172   ,opacity=1 ]  $f_{m}^{\ell}$;

Contour of a morphism, composition of contours, and identity contours.

Contouring extends to a functor from the category of polycategories to the category of categories,
$𝓒 \colon \mathbf{PolyCat} \to \mathbf{Cat}$.

§.§ Malleable Polycategories

A malleable polycategory is a polycategory 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 for composition.

The (1,1)-polymorphisms of a  $ℙ$ form an underlying category $ℙᵘ$.
The polymorphisms form profunctors over the  and their composition, in its four possible forms, is dinatural with respect to the underlying category.
This means that the following four operations are well-defined:

\begin{align*}
(⨾)_1 &፡ {\textstyle \left( ∫^{X ∈ ℙᵘ} ℙ(Γ; Δ, X) × ℙ(X , Γ'; Δ') \right) → ℙ(Γ, Γ'; Δ, Δ'),} \\
(⨾)_2 &፡ {\textstyle \left( ∫^{X ∈ ℙᵘ} ℙ(Γ; X, Δ) × ℙ(Γ', X; Δ') \right) → ℙ(Γ, Γ'; Δ, Δ'),} \\
(⨾)_3 &፡ {\textstyle \left( ∫^{X ∈ ℙᵘ} ℙ(Γ; Δ₁, X, Δ₂) × ℙ(X; Δ) \right) → ℙ(Γ; Δ₁, Δ, Δ₂),} \\
(⨾)_4 &፡ {\textstyle \left( ∫^{X ∈ ℙᵘ} ℙ(Γ;X) × ℙ(Γ₁, X, Γ₂; Δ) \right) → ℙ(Γ₁, Γ, Γ₂; Δ).}
\end{align*}

A malleable polycategory is a  where dinatural composition, in all its four forms, is invertible.

If a  is malleable, we can reconstruct it up to isomorphism from its binary, cobinary, nullary and conullary maps.
When defining a , it is usually easier to provide these binary, cobinary, unary, nullary and conullary maps, and deduce from those the rest of the structure. The situation is now similar to that of linearly distributive categories: we do not need to provide all n-ary tensors in order to define a linearly distributive category, we only provide the binary $(⊗,⅋)$ and unary $(I,Z)$ 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 polycategories are what we will call prostar autonomous categories.

§.§ Prostar-Autonomous Categories

Prostar-autonomous categories provide an algebra for both coherent composition and decomposition.
Apart from the usual morphisms, $𝕍(X; Y)$; and the joints, $𝕍(X₀ ⊗ X₁ ; Y)$, and units, $𝕍(⊤; Y)$, of a ; a prostar-autonomous category has splits, $𝕍(X ; Y₀ ⅋ Y₁)$, and atoms, $𝕍(X ; ⊥)$. As in the case of , these compositions and decompositions must be coherent, which translates into the existence of natural isomorphisms witnessing a Frobenius rule, the Frobenius distributors

\begin{align*}
& \textstyle \varphi_l \colon ∫^{W} ℂ(A ; C ⅋ W) × ℂ(W ⊗ B ; D)
\xrightarrow[]{\cong}
ℂ(A ⊗ B; C ⅋ D),\mbox{ and } \\
& \textstyle \varphi_r \colon ∫^{W} ℂ(A ⊗ W ; C) × ℂ(B ; W ⅋ D)
\xrightarrow[]{\cong}
ℂ(A ⊗ B; C ⅋ D).
\end{align*}

In summary, after this section, we will have developed the relation between malleability and profunctorial structures in an analogous way for both multicategories and polycategories.

Multicategory     Malleable Multicategory     Promonoidal category
Polycategory     Malleable Polycategory     Prostar autonomous category

Prostar-autonomous categories are the 2-Frobenius monoids of the monoidal bicategory of profunctors, which is equivalent to the following definition.
A prostar autonomous category is a category $ℂ$ endowed with a promonoidal structure $(ℂ,⊗,⊤)$, and procomonoidal structure $(ℂ,⅋,⊥)$, that interact as a Frobenius pseudomonoid <cit.>.
That is, it is a category endowed with four profunctors, suggestively written $ℂ(\bullet ⊗ \bullet ; \bullet)$, $ℂ(\top; \bullet)$, $ℂ(\bullet ; \bot)$ and $ℂ(\bullet ; \bullet \parr \bullet)$, as if they were representable. These profunctors form two promonoidal categories <cit.> with coherent associators and unitors. Further, they are endowed with invertible Frobenius distributors,

\begin{align*}
& \textstyle \varphi_l \colon ∫^{W} ℂ(A ; C ⅋ W) × ℂ(W ⊗ B ; D)
\xrightarrow[]{\cong}
ℂ(A ⊗ B; C ⅋ D), \\
& \textstyle \varphi_r \colon ∫^{W} ℂ(A ⊗ W ; C) × ℂ(B ; W ⅋ D)
\xrightarrow[]{\cong}
ℂ(A ⊗ B; C ⅋ D),
\end{align*}

such that every formal diagram formed of these distributors and promonoidal coherences commutes.

have a canonical prostar given by profunctors $ℂ(• ⊗ •; ⊥)$ and $ℂ(⊤; • \parr •)$. We may think of a  as a category $ℂ$ equipped with sets of polymorphisms $ℂ(• ⊗ ... ⊗ • ; • \parr ... \parr •)$. The Frobenius isomorphisms let us decompose polymorphisms into combinations of the pro(co)monoidal structures: this decomposition is unique up to dinaturality. Informally,  are to  what promonoidal categories are to (co)multicategories.

A prostar functor $F \colon 𝕍 \to 𝕎$ is a quintuple $(F_{obj},F_{\otimes},F_{\parr},F_{\top},F_{\bot})$ where $(F_{obj},F_\otimes,F_\top)$ and $(F_{obj}, F_\parr, F_\bot)$ are promonoidal functors that together strictly preserve the Frobenius distributors, in that
$\varphi_l ⨾ (F_\otimes × F_\parr) = (F_\parr × F_\otimes) ⨾ \varphi_l'$ and $\varphi_r ⨾ (F_\otimes × F_\parr) = (F_\otimes × F_\parr) ⨾ \varphi_r'$.
Prostar functors between  form a category, $\mathbf{ProStar}$.

§.§ Prostar Autonomous are Malleable Polycategories

In this section, we show that the category of  is equivalent to that of malleable polycategories. In this sense, the study of malleable polycategories is the study of prostar autonomous categories.

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

\begin{align*}
𝕎^m(X₀,X₁,Γ; Δ) &= \textstyle{∫^V 𝕎(X₀ ⊗ X₁; V) × 𝕎^m(V,Γ;Δ)}, \\
𝕎^m(;Δ) &= \textstyle{∫^V 𝕎(⊤;V) × 𝕎(V;Δ)}, \\
𝕎^m(X;Y₀,Y₁,Δ) &= \textstyle{∫^V 𝕎^m(X;V,Δ) × 𝕎(V;Y₀ ⅋ Y₁)}, \\
𝕎^m(X;) &= \textstyle{𝕎(X;⊥)}.
\end{align*}

In other words, the polymorphisms are elements of the left-biased tree reductions of the promonoidal category, seen as a 2-monoid.
The four forms of dinatural composition are then defined to be the unique map relating two tree expressions in a 2-Frobenius monoid, which exist uniquely by coherence,

\begin{align*}
(\mathrm{coh})_1 &፡ {\textstyle \left( ∫^{X ∈ 𝕎ᵐ} 𝕎ᵐ(Γ; Δ, X) × 𝕎ᵐ(X , Γ'; Δ') \right) → 𝕎ᵐ(Γ, Γ'; Δ, Δ'),} \\
(\mathrm{coh})_2 &፡ {\textstyle \left( ∫^{X ∈ 𝕎ᵐ} 𝕎ᵐ(Γ; X, Δ) × 𝕎ᵐ(Γ', X; Δ') \right) → 𝕎ᵐ(Γ, Γ'; Δ, Δ'),} \\
(\mathrm{coh})_3 &፡ {\textstyle \left( ∫^{X ∈ 𝕎ᵐ} 𝕎ᵐ(Γ; Δ₁, X, Δ₂) × 𝕎ᵐ(X; Δ) \right) → 𝕎ᵐ(Γ; Δ₁, Δ, Δ₂),} \\
(\mathrm{coh})_4 &፡ {\textstyle \left( ∫^{X ∈ 𝕎ᵐ} 𝕎ᵐ(Γ;X) × 𝕎ᵐ(Γ₁, X, Γ₂; Δ) \right) → 𝕎ᵐ(Γ₁, Γ, Γ₂; Δ).}
\end{align*}

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

The category of  and the category of  are equivalent with the functor $(•)ᵐ ፡ \ProStar{} → \mathbf{mPoly}$ induced by the construction of the underlying malleable polycategory of a .  This is the polycategorical analogue of <Ref>.

First, let us show that a , $F ፡ 𝕍 → 𝕎$, induces a polyfunctor, $Fᵐ ፡ 𝕍ᵐ → 𝕎ᵐ$, between the Underlying polycategories. On objects, we define it to be the same, $Fᵐ_{obj} = F_{obj}$. On polymorphisms, we can define the binary, nullary, cobinary, conullary and unary using the  structure,

$$F_{2,1}^m = F_{⊗};\ F_{0,1}^m = F_⊤;\ F_{1,2}^m = F_{⅋};\ F_{1,0}^m = F_⊥; \mbox{ and } F_{1,1}^m = F.$$

§.§ Splice of a Polycategory

Let $ℂ$ be a category. Its  of spliced arrows, $Sℂ$, has underlying category $ℂ^{\text{op}} × ℂ$. Intuitively, its profunctors are defined by spliced circles of morphisms.

every picture/.style=line width=1.2pt

(21,57) .. controls (21,40.43) and (34.43,27) .. (51,27) .. controls (67.57,27) and (81,40.43) .. (81,57) .. controls (81,73.57) and (67.57,87) .. (51,87) .. controls (34.43,87) and (21,73.57) .. (21,57) – cycle ;

[fill=rgb, 255:red, 94; green, 129; blue, 172   ,fill opacity=0.2 ] (51,27) .. controls (54.69,27) and (58.23,27.67) .. (61.49,28.89) .. controls (60.21,32.01) and (59.5,35.42) .. (59.5,39) .. controls (59.5,51.5) and (68.15,62.02) .. (79.9,65.09) .. controls (78.26,70.93) and (74.91,76.05) .. (70.41,79.87) .. controls (65.44,75.01) and (58.58,72) .. (51,72) .. controls (43.42,72) and (36.56,75.01) .. (31.59,79.87) .. controls (27.09,76.05) and (23.74,70.93) .. (22.1,65.09) .. controls (33.85,62.02) and (42.5,51.5) .. (42.5,39) .. controls (42.5,35.42) and (41.79,32.01) .. (40.51,28.89) .. controls (43.77,27.67) and (47.31,27) .. (51,27) – cycle ;

(61.79,49.43) – (63.38,52.26) ;
[shift=(64.36,54), rotate = 240.64] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0] (18,24) – (84,24) – (84,90) – (18,90) – cycle ;

(53.5,72) – (50.61,72.16) ;
[shift=(48.61,72.27), rotate = 356.82] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(38.9,53.1) – (39.72,51.14) ;
[shift=(40.5,49.3), rotate = 112.83] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(101.5,57) .. controls (101.5,73.57) and (114.93,87) .. (131.5,87) .. controls (148.07,87) and (161.5,73.57) .. (161.5,57) .. controls (161.5,40.43) and (148.07,27) .. (131.5,27) .. controls (114.93,27) and (101.5,40.43) .. (101.5,57) – cycle ;

[fill=rgb, 255:red, 94; green, 129; blue, 172   ,fill opacity=0.2 ] (131.5,87) .. controls (135.19,87) and (138.73,86.33) .. (141.99,85.11) .. controls (140.71,81.99) and (140,78.58) .. (140,75) .. controls (140,62.5) and (148.65,51.98) .. (160.4,48.91) .. controls (158.76,43.07) and (155.41,37.95) .. (150.91,34.13) .. controls (145.94,38.99) and (139.08,42) .. (131.5,42) .. controls (123.92,42) and (117.06,38.99) .. (112.09,34.13) .. controls (107.59,37.95) and (104.24,43.07) .. (102.6,48.91) .. controls (114.35,51.98) and (123,62.5) .. (123,75) .. controls (123,78.58) and (122.29,81.99) .. (121.01,85.11) .. controls (124.27,86.33) and (127.81,87) .. (131.5,87) – cycle ;

(144.75,59.81) – (144.14,60.84) ;
[shift=(143.13,62.56), rotate = 300.58] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(131.5,42) – (132.5,42) ;
[shift=(134.5,42), rotate = 180] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(120.5,63.29) – (120.13,62.7) ;
[shift=(119.07,61), rotate = 57.99] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(182.5,57) .. controls (182.5,40.43) and (195.93,27) .. (212.5,27) .. controls (229.07,27) and (242.5,40.43) .. (242.5,57) .. controls (242.5,73.57) and (229.07,87) .. (212.5,87) .. controls (195.93,87) and (182.5,73.57) .. (182.5,57) – cycle ;

[fill=rgb, 255:red, 94; green, 129; blue, 172   ,fill opacity=0.2 ] (212.5,27) .. controls (216.27,27) and (219.89,27.7) .. (223.21,28.97) .. controls (220.15,37.82) and (218.5,47.23) .. (218.5,57) .. controls (218.5,66.77) and (220.15,76.18) .. (223.21,85.03) .. controls (219.89,86.3) and (216.27,87) .. (212.5,87) .. controls (208.73,87) and (205.11,86.3) .. (201.79,85.03) .. controls (204.85,76.18) and (206.5,66.77) .. (206.5,57) .. controls (206.5,47.23) and (204.85,37.82) .. (201.79,28.97) .. controls (205.11,27.7) and (208.73,27) .. (212.5,27) – cycle ;

(206.5,57) – (206.5,56) ;
[shift=(206.5,54), rotate = 90] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(218.5,54) – (218.5,55) ;
[shift=(218.5,57), rotate = 270] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[fill=rgb, 255:red, 94; green, 129; blue, 172   ,fill opacity=0.2 ] (294,27) .. controls (297.77,27) and (301.39,27.7) .. (304.71,28.97) .. controls (304.71,35.05) and (299.92,39.97) .. (294,39.97) .. controls (288.08,39.97) and (283.29,35.05) .. (283.29,28.97) .. controls (286.61,27.7) and (290.23,27) .. (294,27) – cycle ;

(292.5,40.08) – (293.84,40.02) ;
[shift=(290.83,39.92), rotate = 0] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(264,57) .. controls (264,40.43) and (277.43,27) .. (294,27) .. controls (310.57,27) and (324,40.43) .. (324,57) .. controls (324,73.57) and (310.57,87) .. (294,87) .. controls (277.43,87) and (264,73.57) .. (264,57) – cycle ;

[fill=rgb, 255:red, 94; green, 129; blue, 172   ,fill opacity=0.2 ] (375,87) .. controls (378.77,87) and (382.39,86.3) .. (385.71,85.03) .. controls (385.71,78.95) and (380.92,74.03) .. (375,74.03) .. controls (369.08,74.03) and (364.29,78.95) .. (364.29,85.03) .. controls (367.61,86.3) and (371.23,87) .. (375,87) – cycle ;

(376.17,73.75) – (375.5,73.79) ;
[shift=(377.5,73.92), rotate = 180] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(345,57) .. controls (345,73.57) and (358.43,87) .. (375,87) .. controls (391.57,87) and (405,73.57) .. (405,57) .. controls (405,40.43) and (391.57,27) .. (375,27) .. controls (358.43,27) and (345,40.43) .. (345,57) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (39.01,28.89) .. controls (39.01,28.06) and (39.68,27.39) .. (40.51,27.39) .. controls (41.33,27.39) and (42.01,28.06) .. (42.01,28.89) .. controls (42.01,29.72) and (41.33,30.39) .. (40.51,30.39) .. controls (39.68,30.39) and (39.01,29.72) .. (39.01,28.89) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (59.99,28.89) .. controls (59.99,28.06) and (60.67,27.39) .. (61.49,27.39) .. controls (62.32,27.39) and (62.99,28.06) .. (62.99,28.89) .. controls (62.99,29.72) and (62.32,30.39) .. (61.49,30.39) .. controls (60.67,30.39) and (59.99,29.72) .. (59.99,28.89) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (78.4,65.09) .. controls (78.4,64.26) and (79.07,63.59) .. (79.9,63.59) .. controls (80.72,63.59) and (81.4,64.26) .. (81.4,65.09) .. controls (81.4,65.92) and (80.72,66.59) .. (79.9,66.59) .. controls (79.07,66.59) and (78.4,65.92) .. (78.4,65.09) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (68.91,79.87) .. controls (68.91,79.05) and (69.58,78.37) .. (70.41,78.37) .. controls (71.24,78.37) and (71.91,79.05) .. (71.91,79.87) .. controls (71.91,80.7) and (71.24,81.37) .. (70.41,81.37) .. controls (69.58,81.37) and (68.91,80.7) .. (68.91,79.87) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (30.09,79.87) .. controls (30.09,79.05) and (30.76,78.37) .. (31.59,78.37) .. controls (32.42,78.37) and (33.09,79.05) .. (33.09,79.87) .. controls (33.09,80.7) and (32.42,81.37) .. (31.59,81.37) .. controls (30.76,81.37) and (30.09,80.7) .. (30.09,79.87) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (20.6,65.09) .. controls (20.6,64.26) and (21.28,63.59) .. (22.1,63.59) .. controls (22.93,63.59) and (23.6,64.26) .. (23.6,65.09) .. controls (23.6,65.92) and (22.93,66.59) .. (22.1,66.59) .. controls (21.28,66.59) and (20.6,65.92) .. (20.6,65.09) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (110.59,34.13) .. controls (110.59,33.3) and (111.26,32.63) .. (112.09,32.63) .. controls (112.92,32.63) and (113.59,33.3) .. (113.59,34.13) .. controls (113.59,34.95) and (112.92,35.63) .. (112.09,35.63) .. controls (111.26,35.63) and (110.59,34.95) .. (110.59,34.13) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (149.41,34.13) .. controls (149.41,33.3) and (150.08,32.63) .. (150.91,32.63) .. controls (151.74,32.63) and (152.41,33.3) .. (152.41,34.13) .. controls (152.41,34.95) and (151.74,35.63) .. (150.91,35.63) .. controls (150.08,35.63) and (149.41,34.95) .. (149.41,34.13) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (158.9,48.91) .. controls (158.9,48.08) and (159.57,47.41) .. (160.4,47.41) .. controls (161.22,47.41) and (161.9,48.08) .. (161.9,48.91) .. controls (161.9,49.74) and (161.22,50.41) .. (160.4,50.41) .. controls (159.57,50.41) and (158.9,49.74) .. (158.9,48.91) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (140.49,85.11) .. controls (140.49,84.28) and (141.17,83.61) .. (141.99,83.61) .. controls (142.82,83.61) and (143.49,84.28) .. (143.49,85.11) .. controls (143.49,85.94) and (142.82,86.61) .. (141.99,86.61) .. controls (141.17,86.61) and (140.49,85.94) .. (140.49,85.11) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (119.51,85.11) .. controls (119.51,84.28) and (120.18,83.61) .. (121.01,83.61) .. controls (121.83,83.61) and (122.51,84.28) .. (122.51,85.11) .. controls (122.51,85.94) and (121.83,86.61) .. (121.01,86.61) .. controls (120.18,86.61) and (119.51,85.94) .. (119.51,85.11) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (101.1,48.91) .. controls (101.1,48.08) and (101.78,47.41) .. (102.6,47.41) .. controls (103.43,47.41) and (104.1,48.08) .. (104.1,48.91) .. controls (104.1,49.74) and (103.43,50.41) .. (102.6,50.41) .. controls (101.78,50.41) and (101.1,49.74) .. (101.1,48.91) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (200.29,28.97) .. controls (200.29,28.14) and (200.96,27.47) .. (201.79,27.47) .. controls (202.61,27.47) and (203.29,28.14) .. (203.29,28.97) .. controls (203.29,29.8) and (202.61,30.47) .. (201.79,30.47) .. controls (200.96,30.47) and (200.29,29.8) .. (200.29,28.97) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (221.71,28.97) .. controls (221.71,28.14) and (222.39,27.47) .. (223.21,27.47) .. controls (224.04,27.47) and (224.71,28.14) .. (224.71,28.97) .. controls (224.71,29.8) and (224.04,30.47) .. (223.21,30.47) .. controls (222.39,30.47) and (221.71,29.8) .. (221.71,28.97) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (200.29,85.03) .. controls (200.29,84.2) and (200.96,83.53) .. (201.79,83.53) .. controls (202.61,83.53) and (203.29,84.2) .. (203.29,85.03) .. controls (203.29,85.86) and (202.61,86.53) .. (201.79,86.53) .. controls (200.96,86.53) and (200.29,85.86) .. (200.29,85.03) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (221.71,85.03) .. controls (221.71,84.2) and (222.39,83.53) .. (223.21,83.53) .. controls (224.04,83.53) and (224.71,84.2) .. (224.71,85.03) .. controls (224.71,85.86) and (224.04,86.53) .. (223.21,86.53) .. controls (222.39,86.53) and (221.71,85.86) .. (221.71,85.03) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (281.79,28.97) .. controls (281.79,28.14) and (282.46,27.47) .. (283.29,27.47) .. controls (284.11,27.47) and (284.79,28.14) .. (284.79,28.97) .. controls (284.79,29.8) and (284.11,30.47) .. (283.29,30.47) .. controls (282.46,30.47) and (281.79,29.8) .. (281.79,28.97) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (303.21,28.97) .. controls (303.21,28.14) and (303.89,27.47) .. (304.71,27.47) .. controls (305.54,27.47) and (306.21,28.14) .. (306.21,28.97) .. controls (306.21,29.8) and (305.54,30.47) .. (304.71,30.47) .. controls (303.89,30.47) and (303.21,29.8) .. (303.21,28.97) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (362.79,85.03) .. controls (362.79,84.2) and (363.46,83.53) .. (364.29,83.53) .. controls (365.11,83.53) and (365.79,84.2) .. (365.79,85.03) .. controls (365.79,85.86) and (365.11,86.53) .. (364.29,86.53) .. controls (363.46,86.53) and (362.79,85.86) .. (362.79,85.03) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (384.21,85.03) .. controls (384.21,84.2) and (384.89,83.53) .. (385.71,83.53) .. controls (386.54,83.53) and (387.21,84.2) .. (387.21,85.03) .. controls (387.21,85.86) and (386.54,86.53) .. (385.71,86.53) .. controls (384.89,86.53) and (384.21,85.86) .. (384.21,85.03) – cycle ;

(38.51,25.49) node [anchor=south east] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $X^{+}$;

(63.49,25.49) node [anchor=south west] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $X^{-}$;

(81.9,68.49) node [anchor=north west][inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Z^{-}$;

(72.41,83.27) node [anchor=north west][inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Z^{+}$;

(20.1,68.49) node [anchor=north east] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Y^{+}$;

(29.59,83.27) node [anchor=north east] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Y^{-}$;

(100.6,45.51) node [anchor=south east] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $X^{+}$;

(110.09,30.73) node [anchor=south east] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $X^{-}$;

(152.91,30.73) node [anchor=south west] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Y^{+}$;

(162.4,45.51) node [anchor=south west] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Y^{-}$;

(119.01,88.51) node [anchor=north east] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Z^{+}$;

(143.99,88.51) node [anchor=north west][inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Z^{-}$;

(199.79,25.57) node [anchor=south east] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $X^{+}$;

(225.21,25.57) node [anchor=south west] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $X^{-}$;

(199.79,88.43) node [anchor=north east] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Y^{+}$;

(225.21,88.43) node [anchor=north west][inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Y^{-}$;

(281.29,25.57) node [anchor=south east] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $X^{+}$;

(306.71,25.57) node [anchor=south west] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $X^{-}$;

(362.29,88.43) node [anchor=north east] [inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Y^{+}$;

(387.71,88.43) node [anchor=north west][inner sep=0.75pt]  [font=,color=rgb, 255:red, 0; green, 0; blue, 0   ,opacity=1 ]  $Y^{-}$;

(36.9,49.7) node [anchor=south east] [inner sep=0.75pt]  [font=]  $f_{0}$;

(57,85.6) node [anchor=south east] [inner sep=0.75pt]  [font=]  $f_{2}$;

(66.36,50.6) node [anchor=south west] [inner sep=0.75pt]  [font=]  $f_{1}$;

(137,37.6) node [anchor=south east] [inner sep=0.75pt]  [font=]  $g_{1}$;

(119,62.4) node [anchor=north east] [inner sep=0.75pt]  [font=]  $g_{0}$;

(145,62.4) node [anchor=north west][inner sep=0.75pt]  [font=]  $g_{2}$;

(193,53.4) node [anchor=north west][inner sep=0.75pt]  [font=]  $h_{0}$;

(220,53.4) node [anchor=north west][inner sep=0.75pt]  [font=]  $h_{1}$;

(289,44.4) node [anchor=north west][inner sep=0.75pt]  [font=]  $k_{0}$;

(370,60.4) node [anchor=north west][inner sep=0.75pt]  [font=]  $l_{0}$;

Explicitly, it is defined by the following profunctors (below, left). The coherence isomorphisms are defined by glueing circles along the desired boundary and composing the relevant arrows; two compositions are isomorphic if and only if they determine the same arrows (below, right).

This structure appeared in Day & Street <cit.>, where it was noticed that the canonical promonoidal category induced by a small category <cit.> has an involution. As a , it was rediscovered by Melliès & Zeilberger <cit.>. Monoidal spliced arrows were explicitly introduced and characterized as an adjunction in a joint work <cit.>.

\begin{align*}
\Splice{(ℂ)} \left( \biobj{X^+}{X^-} ;  \biobj{Y^+}{Y^-} ⅋ \biobj{Z^+}{Z^-}\right) & =
ℂ(Y^+; X^+) × ℂ(X^-; Z^-) × ℂ(Z^+; Y^-); \\
\Splice{(ℂ)} \left( \biobj{X^+}{X^-} ⊗ \biobj{Y^+}{Y^-} ; \biobj{Z^+}{Z^-}\right) & =
ℂ(Z^+; X^+) × ℂ(X^-; Y^+) × ℂ(Y^-; Z^-); \\
\Splice{(ℂ)} \left( \biobj{X^+}{X^-} ; \biobj{Y^+}{Y^-} \right) & =
ℂ(Y^+; X^+) × ℂ(X^-; Y^-); \\
\Splice{(ℂ)} \left( \biobj{X^+}{X^-} ; \bot \right) & =
ℂ(X^-; X^+); \\
\Splice{(ℂ)} \left(\top ; \biobj{Y^+}{Y^-}  \right) & =
ℂ(Y^+; Y^-). \\
\end{align*}

every picture/.style=line width=1pt

(39,17.13) .. controls (55.57,17.13) and (69,30.56) .. (69,47.13) .. controls (69,49.98) and (68.6,52.73) .. (67.86,55.34) .. controls (73.11,50.85) and (79.92,48.13) .. (87.37,48.13) .. controls (103.94,48.13) and (117.37,61.56) .. (117.37,78.13) .. controls (117.37,94.7) and (103.94,108.13) .. (87.37,108.13) .. controls (70.81,108.13) and (57.37,94.7) .. (57.37,78.13) .. controls (57.37,75.28) and (57.77,72.52) .. (58.51,69.91) .. controls (53.27,74.41) and (46.45,77.13) .. (39,77.13) .. controls (22.43,77.13) and (9,63.69) .. (9,47.13) .. controls (9,30.56) and (22.43,17.13) .. (39,17.13) – cycle ;

[fill=rgb, 255:red, 94; green, 129; blue, 172   ,fill opacity=0.2 ] (39,17.13) .. controls (42.69,17.13) and (46.23,17.79) .. (49.49,19.01) .. controls (48.21,22.14) and (47.5,25.55) .. (47.5,29.13) .. controls (47.5,41.62) and (56.15,52.14) .. (67.9,55.22) .. controls (67.88,55.26) and (67.87,55.3) .. (67.86,55.34) .. controls (67.89,55.31) and (67.93,55.29) .. (67.96,55.26) .. controls (72.94,60.12) and (79.8,63.13) .. (87.37,63.13) .. controls (94.95,63.13) and (101.81,60.12) .. (106.79,55.26) .. controls (111.28,59.08) and (114.64,64.2) .. (116.27,70.04) .. controls (104.53,73.11) and (95.87,83.63) .. (95.87,96.13) .. controls (95.87,99.71) and (96.58,103.12) .. (97.87,106.24) .. controls (94.6,107.46) and (91.07,108.13) .. (87.37,108.13) .. controls (83.68,108.13) and (80.15,107.46) .. (76.88,106.24) .. controls (78.17,103.12) and (78.87,99.71) .. (78.87,96.13) .. controls (78.87,83.63) and (70.22,73.11) .. (58.48,70.04) .. controls (58.49,70) and (58.5,69.95) .. (58.51,69.91) .. controls (58.48,69.94) and (58.45,69.97) .. (58.41,70) .. controls (53.44,65.13) and (46.58,62.13) .. (39,62.13) .. controls (31.42,62.13) and (24.56,65.13) .. (19.59,70) .. controls (15.09,66.18) and (11.74,61.06) .. (10.1,55.22) .. controls (21.85,52.14) and (30.5,41.62) .. (30.5,29.13) .. controls (30.5,25.55) and (29.79,22.14) .. (28.51,19.01) .. controls (31.77,17.79) and (35.31,17.13) .. (39,17.13) – cycle ;

(49.79,39.55) – (51.38,42.38) ;
[shift=(52.36,44.13), rotate = 240.64] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0] (6,14.13) – (72,14.13) – (72,80.13) – (6,80.13) – cycle ;

(41.5,62.13) – (38.61,62.29) ;
[shift=(36.61,62.4), rotate = 356.82] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(26.9,43.22) – (27.72,41.27) ;
[shift=(28.5,39.43), rotate = 112.83] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (27.01,19.01) .. controls (27.01,18.18) and (27.68,17.51) .. (28.51,17.51) .. controls (29.33,17.51) and (30.01,18.18) .. (30.01,19.01) .. controls (30.01,19.84) and (29.33,20.51) .. (28.51,20.51) .. controls (27.68,20.51) and (27.01,19.84) .. (27.01,19.01) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (47.99,19.01) .. controls (47.99,18.18) and (48.67,17.51) .. (49.49,17.51) .. controls (50.32,17.51) and (50.99,18.18) .. (50.99,19.01) .. controls (50.99,19.84) and (50.32,20.51) .. (49.49,20.51) .. controls (48.67,20.51) and (47.99,19.84) .. (47.99,19.01) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (66.4,55.22) .. controls (66.4,54.39) and (67.07,53.72) .. (67.9,53.72) .. controls (68.72,53.72) and (69.4,54.39) .. (69.4,55.22) .. controls (69.4,56.04) and (68.72,56.72) .. (67.9,56.72) .. controls (67.07,56.72) and (66.4,56.04) .. (66.4,55.22) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (56.91,70) .. controls (56.91,69.17) and (57.58,68.5) .. (58.41,68.5) .. controls (59.24,68.5) and (59.91,69.17) .. (59.91,70) .. controls (59.91,70.83) and (59.24,71.5) .. (58.41,71.5) .. controls (57.58,71.5) and (56.91,70.83) .. (56.91,70) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (18.09,70) .. controls (18.09,69.17) and (18.76,68.5) .. (19.59,68.5) .. controls (20.42,68.5) and (21.09,69.17) .. (21.09,70) .. controls (21.09,70.83) and (20.42,71.5) .. (19.59,71.5) .. controls (18.76,71.5) and (18.09,70.83) .. (18.09,70) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (8.6,55.22) .. controls (8.6,54.39) and (9.28,53.72) .. (10.1,53.72) .. controls (10.93,53.72) and (11.6,54.39) .. (11.6,55.22) .. controls (11.6,56.04) and (10.93,56.72) .. (10.1,56.72) .. controls (9.28,56.72) and (8.6,56.04) .. (8.6,55.22) – cycle ;

(100.62,80.94) – (100.02,81.97) ;
[shift=(99,83.69), rotate = 300.58] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(87.37,63.13) – (88.37,63.13) ;
[shift=(90.37,63.13), rotate = 180] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(76.37,84.42) – (76.01,83.83) ;
[shift=(74.95,82.13), rotate = 57.99] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (66.46,55.26) .. controls (66.46,54.43) and (67.13,53.76) .. (67.96,53.76) .. controls (68.79,53.76) and (69.46,54.43) .. (69.46,55.26) .. controls (69.46,56.08) and (68.79,56.76) .. (67.96,56.76) .. controls (67.13,56.76) and (66.46,56.08) .. (66.46,55.26) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (105.29,55.26) .. controls (105.29,54.43) and (105.96,53.76) .. (106.79,53.76) .. controls (107.61,53.76) and (108.29,54.43) .. (108.29,55.26) .. controls (108.29,56.08) and (107.61,56.76) .. (106.79,56.76) .. controls (105.96,56.76) and (105.29,56.08) .. (105.29,55.26) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (114.77,70.04) .. controls (114.77,69.21) and (115.44,68.54) .. (116.27,68.54) .. controls (117.1,68.54) and (117.77,69.21) .. (117.77,70.04) .. controls (117.77,70.87) and (117.1,71.54) .. (116.27,71.54) .. controls (115.44,71.54) and (114.77,70.87) .. (114.77,70.04) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (96.37,106.24) .. controls (96.37,105.42) and (97.04,104.74) .. (97.87,104.74) .. controls (98.7,104.74) and (99.37,105.42) .. (99.37,106.24) .. controls (99.37,107.07) and (98.7,107.74) .. (97.87,107.74) .. controls (97.04,107.74) and (96.37,107.07) .. (96.37,106.24) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (75.38,106.24) .. controls (75.38,105.42) and (76.05,104.74) .. (76.88,104.74) .. controls (77.71,104.74) and (78.38,105.42) .. (78.38,106.24) .. controls (78.38,107.07) and (77.71,107.74) .. (76.88,107.74) .. controls (76.05,107.74) and (75.38,107.07) .. (75.38,106.24) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (56.98,70.04) .. controls (56.98,69.21) and (57.65,68.54) .. (58.48,68.54) .. controls (59.31,68.54) and (59.98,69.21) .. (59.98,70.04) .. controls (59.98,70.87) and (59.31,71.54) .. (58.48,71.54) .. controls (57.65,71.54) and (56.98,70.87) .. (56.98,70.04) – cycle ;

[draw opacity=0] (6,14.13) – (120,14.13) – (120,110.13) – (6,110.13) – cycle ;

(198,89.13) .. controls (198,105.69) and (184.57,119.13) .. (168,119.13) .. controls (151.43,119.13) and (138,105.69) .. (138,89.13) .. controls (138,76.32) and (146.02,65.39) .. (157.31,61.09) .. controls (145.95,56.81) and (137.88,45.85) .. (137.88,33) .. controls (137.88,16.43) and (151.31,3) .. (167.88,3) .. controls (184.44,3) and (197.88,16.43) .. (197.88,33) .. controls (197.88,45.8) and (189.86,56.73) .. (178.57,61.04) .. controls (189.92,65.31) and (198,76.28) .. (198,89.13) – cycle ;

[fill=rgb, 255:red, 94; green, 129; blue, 172   ,fill opacity=0.2 ] (178.49,61.01) .. controls (177.21,64.14) and (176.5,67.55) .. (176.5,71.13) .. controls (176.5,83.62) and (185.15,94.14) .. (196.9,97.22) .. controls (195.26,103.06) and (191.91,108.18) .. (187.41,112) .. controls (182.44,107.13) and (175.58,104.13) .. (168,104.13) .. controls (160.42,104.13) and (153.56,107.13) .. (148.59,112) .. controls (144.09,108.18) and (140.74,103.06) .. (139.1,97.22) .. controls (150.85,94.14) and (159.5,83.62) .. (159.5,71.13) .. controls (159.5,67.62) and (158.82,64.26) .. (157.58,61.19) .. controls (157.51,61.16) and (157.45,61.14) .. (157.38,61.11) .. controls (158.67,57.99) and (159.38,54.58) .. (159.38,51) .. controls (159.38,38.5) and (150.72,27.98) .. (138.98,24.91) .. controls (140.61,19.07) and (143.97,13.95) .. (148.46,10.13) .. controls (153.44,14.99) and (160.3,18) .. (167.88,18) .. controls (175.45,18) and (182.31,14.99) .. (187.29,10.13) .. controls (191.78,13.95) and (195.14,19.07) .. (196.77,24.91) .. controls (185.03,27.98) and (176.38,38.5) .. (176.38,51) .. controls (176.38,54.51) and (177.06,57.86) .. (178.3,60.94) .. controls (178.36,60.96) and (178.43,60.99) .. (178.49,61.01) – cycle ;

(178.79,81.55) – (180.38,84.38) ;
[shift=(181.36,86.13), rotate = 240.64] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0] (135,56.13) – (201,56.13) – (201,122.13) – (135,122.13) – cycle ;

(170.5,104.13) – (167.61,104.29) ;
[shift=(165.61,104.4), rotate = 356.82] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(155.9,85.23) – (156.72,83.27) ;
[shift=(157.5,81.43), rotate = 112.83] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (156.01,61.01) .. controls (156.01,60.18) and (156.68,59.51) .. (157.51,59.51) .. controls (158.33,59.51) and (159.01,60.18) .. (159.01,61.01) .. controls (159.01,61.84) and (158.33,62.51) .. (157.51,62.51) .. controls (156.68,62.51) and (156.01,61.84) .. (156.01,61.01) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (176.99,61.01) .. controls (176.99,60.18) and (177.67,59.51) .. (178.49,59.51) .. controls (179.32,59.51) and (179.99,60.18) .. (179.99,61.01) .. controls (179.99,61.84) and (179.32,62.51) .. (178.49,62.51) .. controls (177.67,62.51) and (176.99,61.84) .. (176.99,61.01) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (195.4,97.22) .. controls (195.4,96.39) and (196.07,95.72) .. (196.9,95.72) .. controls (197.72,95.72) and (198.4,96.39) .. (198.4,97.22) .. controls (198.4,98.04) and (197.72,98.72) .. (196.9,98.72) .. controls (196.07,98.72) and (195.4,98.04) .. (195.4,97.22) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (185.91,112) .. controls (185.91,111.17) and (186.58,110.5) .. (187.41,110.5) .. controls (188.24,110.5) and (188.91,111.17) .. (188.91,112) .. controls (188.91,112.83) and (188.24,113.5) .. (187.41,113.5) .. controls (186.58,113.5) and (185.91,112.83) .. (185.91,112) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (147.09,112) .. controls (147.09,111.17) and (147.76,110.5) .. (148.59,110.5) .. controls (149.42,110.5) and (150.09,111.17) .. (150.09,112) .. controls (150.09,112.83) and (149.42,113.5) .. (148.59,113.5) .. controls (147.76,113.5) and (147.09,112.83) .. (147.09,112) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (137.6,97.22) .. controls (137.6,96.39) and (138.28,95.72) .. (139.1,95.72) .. controls (139.93,95.72) and (140.6,96.39) .. (140.6,97.22) .. controls (140.6,98.04) and (139.93,98.72) .. (139.1,98.72) .. controls (138.28,98.72) and (137.6,98.04) .. (137.6,97.22) – cycle ;

(181.13,35.81) – (180.52,36.84) ;
[shift=(179.5,38.56), rotate = 300.58] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(167.88,18) – (168.88,18) ;
[shift=(170.88,18), rotate = 180] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

(156.88,39.29) – (156.51,38.7) ;
[shift=(155.45,37), rotate = 57.99] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (4.37,-1.32) .. controls (2.78,-0.56) and (1.32,-0.12) .. (0,0) .. controls (1.32,0.12) and (2.78,0.56) .. (4.37,1.32)   ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (146.96,10.13) .. controls (146.96,9.3) and (147.64,8.63) .. (148.46,8.63) .. controls (149.29,8.63) and (149.96,9.3) .. (149.96,10.13) .. controls (149.96,10.95) and (149.29,11.63) .. (148.46,11.63) .. controls (147.64,11.63) and (146.96,10.95) .. (146.96,10.13) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (185.79,10.13) .. controls (185.79,9.3) and (186.46,8.63) .. (187.29,8.63) .. controls (188.11,8.63) and (188.79,9.3) .. (188.79,10.13) .. controls (188.79,10.95) and (188.11,11.63) .. (187.29,11.63) .. controls (186.46,11.63) and (185.79,10.95) .. (185.79,10.13) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (195.27,24.91) .. controls (195.27,24.08) and (195.94,23.41) .. (196.77,23.41) .. controls (197.6,23.41) and (198.27,24.08) .. (198.27,24.91) .. controls (198.27,25.74) and (197.6,26.41) .. (196.77,26.41) .. controls (195.94,26.41) and (195.27,25.74) .. (195.27,24.91) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (176.87,61.11) .. controls (176.87,60.28) and (177.54,59.61) .. (178.37,59.61) .. controls (179.2,59.61) and (179.87,60.28) .. (179.87,61.11) .. controls (179.87,61.94) and (179.2,62.61) .. (178.37,62.61) .. controls (177.54,62.61) and (176.87,61.94) .. (176.87,61.11) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (155.88,61.11) .. controls (155.88,60.28) and (156.55,59.61) .. (157.38,59.61) .. controls (158.21,59.61) and (158.88,60.28) .. (158.88,61.11) .. controls (158.88,61.94) and (158.21,62.61) .. (157.38,62.61) .. controls (156.55,62.61) and (155.88,61.94) .. (155.88,61.11) – cycle ;

[draw opacity=0][fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (137.48,24.91) .. controls (137.48,24.08) and (138.15,23.41) .. (138.98,23.41) .. controls (139.81,23.41) and (140.48,24.08) .. (140.48,24.91) .. controls (140.48,25.74) and (139.81,26.41) .. (138.98,26.41) .. controls (138.15,26.41) and (137.48,25.74) .. (137.48,24.91) – cycle ;

[draw opacity=0] (117,47.13) – (144,47.13) – (144,74.13) – (117,74.13) – cycle ;

(24.9,39.82) node [anchor=south east] [inner sep=0.75pt]  [font=]  $f_{0}$;

(45,74.72) node [anchor=south east] [inner sep=0.75pt]  [font=]  $f_{2}$;

(54.36,40.72) node [anchor=south west] [inner sep=0.75pt]  [font=]  $f_{1}$;

(92.87,58.73) node [anchor=south east] [inner sep=0.75pt]  [font=]  $g_{1}$;

(74.87,83.53) node [anchor=north east] [inner sep=0.75pt]  [font=]  $g_{0}$;

(100.87,83.53) node [anchor=north west][inner sep=0.75pt]  [font=]  $g_{2}$;

(153.9,81.82) node [anchor=south east] [inner sep=0.75pt]  [font=]  $k_{0}$;

(174,116.73) node [anchor=south east] [inner sep=0.75pt]  [font=]  $k_{2}$;

(183.36,82.73) node [anchor=south west] [inner sep=0.75pt]  [font=]  $k_{1}$;

(173.38,13.6) node [anchor=south east] [inner sep=0.75pt]  [font=]  $h_{1}$;

(155.38,38.4) node [anchor=north east] [inner sep=0.75pt]  [font=]  $h_{0}$;

(181.38,38.4) node [anchor=north west][inner sep=0.75pt]  [font=]  $h_{2}$;

(130.5,60.63) node  [font=]  $\overset{\phi_1}\sim $;

Holds if $f₀ = k₀ ⨾ h₀$, $f₁ ⨾ g₁ = h₁$, $g₂ = h₂ ⨾ k₁$, $g₀ ⨾ f₂ = k₂$.

$\Splice{(ℂ)}$ has a representable prostar, given on objects by

$$\left( \biobj{X^+}{X^-} \right)^{*} = \left( \biobj{X^-}{X^+} \right).$$

Spliced arrows extend to a functor, $\Splice{} : \mathbf{Cat}{} \to \ProStarAut{}$.

Contour extends to a functor $\Contour{} \colon \mathbf{PolyCat} \to \Cat{}$, splice extends to a functor $\Splice \colon \Cat{} \to \ProStarAut{}$. $\Contour{}$ is left adjoint to $\Splice{}$ composed with the forgetful functor, $\Contour{} \dashv \Splice{} ⨾ \mathsf{Forget}$; and $\Contour{}$ composed with the forgetful functor is left adjoint to $\Splice{}$, meaning $\mathsf{Forget} ⨾ \Contour{} \dashv \Splice{}$.

The proof extends our previous one <cit.>.

§.§ Bibliography

were defined by Szabo <cit.> in the symmetric case; Cockett and Seely contributed the planar version we study here <cit.>.

Street <cit.> prove that Frobenius pseudomonoids in $\mathbf{Prof}$ are equivalent to what Day & Street  <cit.> call “$\ast$-autonomous promonoidal categories”. The minor twist we take, “prostar autonomous”, emphasizes that the canonical prostar may not be representable. When all of the structure including the prostar is representable, we obtain $\ast$-autonomous categories.