We present a categorical construction for modelling causal structures within a general class of process theories that include classical probability theory and quantum theory. Unlike prior constructions within categorical quantum mechanics, the objects of this theory encode fine-grained causal relationships between subsystems and give a new method for expressing and deriving consequences for a broad class of causal structures. To illustrate this point, we show that this framework enables one to express consistency with arbitrary (acyclic) causal orderings. In particular, one can define one-way signalling (a.k.a. semi-causal) processes, non-signalling processes, and quantum $n$-combs. Furthermore, our framework is general enough to define families of processes which still behave locally like e.g., classical and quantum theory, but globally allow indefinite causal orderings, such as the quantum switch and the process matrices of Oreshkov, Costa, and Brukner. After defining these families of causal structures within our framework, we give derivations of their operational behaviour using simple, diagrammatic axioms.

§ INTRODUCTION

Broadly, causal structures identify which events or processes taking place across space and time can, in principle, serve as causes or effects of one another. In the field of statistical causal inference, directed acyclic graphs (or generalisations thereof) have been used to capture that fact that certain random variables may have causal influences on others. That is, forcefully changing a certain variable (e.g., whether a patient takes a drug or placebo in randomised trial) may have an effect on another variable (e.g., whether the patient recovers). Intuitively, it may seem impossible to draw such causal conclusions without making such an intervention, however it has been shown in recent years that, under certain assumptions, one can draw causal conclusions purely from observational data [32]. For instance, the constraint-based approach to causal discovery uses conditional independences present in statistical data to iteratively rule out possible causal relationships by removing edges from a (typically very large) directed graph. This sits at the heart of modern, graph-based causal discovery algorithms such as FCI [38], and has been successful in a wide variety of real-world applications, including the study of ADHD [37], neural connectivity [20], gene regulation networks [35], and climate change [18].

In recent years, it has been asked whether, and to what extent, concepts from classical causal reasoning can be transferred to quantum theory, or more generalised theories of interacting processes. A major obstacle to employing classical techniques comes from the presence of quantum non-locality, i.e., the possibility of correlations observed between distant, non-communicating agents which cannot be explained by a classical common cause. Indeed, Wood and Spekkens showed that quantum theory allows correlations which admit no faithful classical causal model [41]. Roughly speaking, this means that any attempt to naïvely reproduce quantum correlations with a classical causal model will necessarily include spurious causal relationships. Hence, there have been numerous attempts to extend classical causal models to quantum [34, 16, 2] or even more general [23] models.

In the context of quantum theory, causal relationships between inputs and outputs to quantum processes have been expressed in a variety of ways. Perhaps the simplest are in the form of non-signalling constraints, which guarantee that distant agents are not capable of sending information faster that the speed of light, e.g., to affect each other's measurement outcomes [4]. Quantum strategies [22] and more recently quantum combs [5] offer a means of expressing more intricate causal relationships, in the form of chains of causally ordered inputs and outputs. Furthermore, it has been shown recently that one can formulate a theory that is locally consistent with quantum theory yet assumes no fixed background causal structure [31]. Interestingly, such a theory admits indefinite causal structures. Namely, it allows one to express processes which inhabit a quantum superposition of causal orders. If physically realisable, such processes can outperform any theory that demands a fixed causal ordering in certain non-local games such as `guess your neighbour's input' [31] and quantum computational tasks such as single-shot channel discrimination [8]. Perhaps even more surprisingly, it has been shown recently that, in the presence of three or more parties, causal bounds can be violated even within a theory that behaves locally like classical probability theory [3]. The key ingredient in studying (and varying) causal structures of processes is the development of a coherent theory of higher order causal processes. That is, if we treat local agents (or events, laboratories, etc.) as first order causal processes, then the act of composing these processes in a particular causal order should be treated as a second-order process.

This paper aims to represent causal relationships within `black box' processes (which could be classical, quantum, or more general) in a uniform way, and provide some of the first tools for `generalised causal reasoning' which can be applied in both the classical and quantum contexts. To do this, we start from a category $\mathcal C$ of `raw materials'—whose morphisms should be thought of as processes without any causal constraints—and construct a new category $\Caus[\mathcal C]$ of first and higher-order processes which are consistent with certain given causal constraints.

For $\mathcal C$, we introduce a new kind of category called a precausal category, which is a compact closed category with a bit of extra structure enabling us to reason about causal relationships between systems.

Most notably, precausal categories have a special discarding process defined on each object, which enables one to say when a process is causal, namely when it satisfies the following equation:

\[ \tikzfig{causal} \]

This has a clear operational intuition:

If the output of a causal process is discarded, it doesn't matter which process occurred.

...or put a slightly different way:

The only influence a causal process has is on its output.

In particular, causality rules out the possibility of hidden side effects or the `backwards flow' of information from a given process.
While seemingly obvious, the causality condition, originally given by [7] in the context of operational probabilistic theories, is surprisingly powerful. For instance, it is equivalent to the non-signalling property for joint processes arising from shared correlations [13].

It is thus natural to consider the subcategory of $\mathcal C$ consisting of all causal processes. However, we take this a step further and consider not only (first-order) causal processes, but also higher-order mappings which preserve certain kinds of causal processes. This yields a $*$-autonomous category , into which the category of all first-order causal processes embeds fully and faithfully. We therefore call categories of the form $\Caus[\mathcal C]$ higher-order causal categories (HOCCs). Our main examples start from the precausal categories of matrices of positive real numbers and completely positive maps, which will yield HOCCs of higher-order classical stochastic processes and higher-order quantum channels, respectively.

While categorical quantum mechanics [1] has typically focussed on compact closed categories of quantum processes, we show that this $*$-autonomous structure yields a much richer type system for describing causal relationships between systems. Whereas compact closed categories have only one way to form joint systems, namely $\otimes$, $*$-autonomous categories have two: $\otimes$ and $\parr$. A simple, yet striking example of the difference in these two connectives in $\Caus[\mathcal C]$ comes from forming types of processes on a joint system:

\begin{align*}
(\bm A \limp \bm A') \otimes (\bm B \limp \bm B') & \ \ \leftarrow\ \textrm{non-signalling processes} \\
(\bm A \limp \bm A') \parr (\bm B \limp \bm B') & \ \ \leftarrow\ \textrm{all processes}
\end{align*}

Using the richer type system afforded by $*$-autonomous categories, we are able to give logical characterisations of many kinds of first- and higher-order causality constraints, and show, for example, when certain constraints imply others.

The paper is structured as follows. In section <ref>, we outline the basics of compact closed categories, string diagrams, $*$-autonomous categories, discarding, and (non-)signalling processes. In section <ref>, we introduce precausal categories and prove some basic properties, such as the no time-travel theorem for precausal categories. In section <ref>, we construct the higher-order causal category $\CausC$ and show that it is $*$-autonomous. In section <ref>, we show that one-way signalling processes can be captured in a HOCC using a generalisation of quantum combs, and processes satisfying arbitrary acyclic causal structures can be captured using pullbacks of combs. In section <ref>, we show that HOCCs also enable us to capture bipartite and $n$-partite second-order causal processes. We give several examples which are known to exhibit indefinite causal structure, namely the OCB process from [31], the classical tripartite process from [3], and an abstract version of the quantum switch defined in [8]. Finally, we prove using just the structure of that the switch does not admit a causal ordering by reducing to no time-travel.

Related work. This work was inspired by [33], which aims for a uniform description of higher-order quantum operations in terms of generalised Choi operators. However, rather than relying on the linear structure of spaces of operators, we work purely in terms of the $*$-autonomous structure and the precausal axioms, which concern the compositional behaviour of discarding processes. The construction of is a variant of the double gluing construction used in [24] to construct models of linear logic. In the language of that paper, our construction consists of building the `tight orthogonality category' induced by a focussed orthogonality on $\{1_I\}\subseteq \mathcal C(I,I)$, and then restricting to objects satisfying the flatness condition in Definition <ref>.
Since it is $*$-autonomous, indeed gives a model of multiplicative linear logic, enabling us to enlist the aid of linear-logic based tools for proving theorems about causal types. We comment briefly on this in the conclusion. When fixing $\mathcal C = \MatRp$, the category $\Caus[\MatRp]$ is closely related to (the finite-dimensional subcategory of) probabilistic coherence spaces, introduced in [21] and refined in [17]. The main difference, aside from allowing matrices over infinite sets of indices, is that the latter defines duals with respect to $[0,1] \subseteq \mathcal \MatRp(I,I) \cong \mathbb R_+$ rather than $\{1\}$, which allows one to capture sub-normalised probability distributions as well as normalised ones.
Our construction indeed extends to incorporate sub-normalised processes, but understanding the structure of the resulting, larger category and its relationship to the one we define is a subject of future work. It is worth noting however, that the correspondence with coherence spaces does not extend to the quantum case. In particular, $\Caus[\CPM]$ is better behaved than the quantum coherence spaces defined by Gerard in [21], as it inherits the quantum tensor product—and hence the usual notions of positivity for states and completely positive for morphisms—from the underlying category $\CPM$.

Acknowledgements. Both authors are grateful to Paulo Perinotti for his input and sharing a draft version of [33]. We would also like to thank Časlav Brukner, Matty Hoban, and Sam Staton for useful discussions. This work is supported by the ERC under the European Union's Seventh Framework Programme (FP7/2007-2013) / ERC grant no 320571.

This is an extended version of a conference paper with the same title [27]. While the overall structure is the same, it has been expanded with additional examples and explanation and provides two new technical contributions. The first is a proof that $\Rel$ is `weakly' precausal, in that it satisfies all of the precausal axioms except . The second and more substantial contribution is the pullback construction in Section <ref> which is used to capture all acyclic causal structures, rather than just linear ones as in [27].

§ PRELIMINARIES

We work in the context of symmetric monoidal categories (SMCs). An SMC consists of a collection of objects $\textrm{ob}(\mathcal C)$, for every pair of objects, $A, B \in \textrm{ob}(\mathcal C)$ a set $\mathcal C(A,B)$ of morphisms, associative sequential composition `$\circ$' with units $1_A$ for all $A \in \textrm{ob}(\mathcal C)$, associative (up to isomorphism) parallel composition `$\otimes$' for objects and morphisms with unit $I \in \textrm{ob}(\mathcal C)$, and swap maps $\sigma_{A,B} : A \otimes B \to B \otimes A$, satisfying the usual equations one would expect for composition and tensor product. For simplicity, we furthermore assume $\mathcal C$ is strict, i.e.

\[
(A \otimes B) \otimes C = A \otimes (B \otimes C) \qquad\qquad A \otimes I = A = I \otimes A \vspace{-0pt}
\]

This is no loss of generality since every SMC is equivalent to a strict one. For details, [30] is a standard reference.

We wish to treat SMCs as theories of physical processes, hence we often refer to objects as systems and morphisms as processes. We will also extensively use string diagram notation for SMCs, where systems are depicted as wires, processes as boxes, and:

\begin{eqnarray*}
g \circ f := \tikzfig{seq-comp} \qquad
f \otimes g := \tikzfig{par-comp}\\
1_A := \tikzfig{wire} \quad
1_I := \emptydiag \quad
\sigma_{A,B} := \tikzfig{swap}
\end{eqnarray*}

Note that diagrams should be read from bottom-to-top. A process $\rho : I \to A$ is called a state, a process $\pi : A \to I$ is called an effect, and $\lambda : I\to I$ is called a number or scalar. Depicted as string diagrams:

\[
\textit{state} := \pointmap{\rho}\quad
\textit{effect} := \copointmap{\pi}\quad
\textit{number} := \lambda
\]

Numbers in an SMC always form a commutative monoid with `multiplication' $\circ$ and unit the identity morphism $1_I$. We typically write $1_I$ simply as $1$.

§.§ Compact closed categories and higher-order string diagrams

We will begin with a category $\mathcal C$ and construct a new category $\CausC$ of higher-order causal processes. In order to make this construction, we first need a mechanism for expressing higher-order processes. Compact closure provides such a mechanism that is convenient within the graphical language and already familiar within the literature on quantum channels, in the guise of the Choi-Jamiołkowski isomorphism.

An SMC $\mathcal C$ is called compact closed if every object $A$ has a dual object $A^{*}$. That is, for every $A$ there exists morphisms $\eta_A: I \to A^{*} \otimes A$ and $\epsilon_A:A \otimes A^{*} \to I$, satisfying:

\begin{equation*}
(\epsilon_A \otimes 1_A) \circ (1_A \otimes \eta_A) = 1_A
\qquad\qquad
(1_{A^*} \otimes \epsilon_A) \circ (\eta_A \otimes 1_{A^*}) = 1_{A^*}
\end{equation*}

We refer to $\eta_A$ and $\epsilon_A$ as a cup and a cap, denoted graphically as cup and cap, respectively. In this notation, the equations in Definition <ref> become:

\[ \tikzfig{line_yank} \qquad\qquad \tikzfig{line_yank2} \]

It is always possible to choose cups and caps in such a way that the canonical isomorphisms $I^* \cong I$, $(A \otimes B)^* \cong A^* \otimes B^*$, and $A \cong A^{**}$ are all in fact equalities. We will assume this is the case throughout this paper.

Crucially, two morphisms in a compact closed category are equal if and only if their string diagrams are the same. That is, if one diagram can be continuously deformed into the other while maintaining the connections between boxes. Hence, when we draw a string diagram, we mean any composition of boxes via cups, caps, and swaps which yields the given diagram, up to deformation. See [36] for an overview of string diagram languages for monoidal categories.

Compact closed categories exhibit process-state duality,
that is, processes $f : A \to B$ are in 1-to-1 correspondence with states $\rho_f : I \to A^* \otimes B$:

\begin{equation}\label{eq:map-state}
\unbig{\boxmap{f}} \ \ \mapsto\ \  \tikzfig{map_to_state}
\end{equation}

Hence, we treat everything as a `state' in $\mathcal C$ and write $f : X$ as shorthand for $f : I \to X$.
In this notation, states are of the form $\rho : A$, effects $\pi : A^*$, and general processes $f : A^* \otimes B$.
Furthermore, we won't require `output' wires to exit upward, and we allow irregularly-shaped boxes.
For example, we can write a process $w : A^* \otimes B \otimes C^* \otimes D$ using `comb' notation:

\begin{equation}\label{eq:comb-versions}
\tikzfig{comb-versions}
\end{equation}

Note that we adopt the convention that an $A$-labelled `input' wire is of the same type as an $A^*$-labelled `output'.

While both the LHS and the RHS in equation (<ref>) are notation for the same process $w$, the LHS is strongly suggestive of a second-order mapping from processes $B \to C$ to processes $A \to D$. Composition in this notation simply means applying the appropriate `cap' processes to plug wires together:

\[ \tikzfig{2_Comb-comp} \]

Since oddly-shaped boxes don't uniquely fix any ordering of systems with respect to $\otimes$, we will often `name' each system by giving it a unique type and assume systems are permuted via $\sigma$-maps whenever necessary. This is a common practice e.g., in the quantum information literature.

Our key examples of compact closed categories to which we will apply our construction to obtain categories of higher-order causal types,
will be and , which we introduce now.
They contain stochastic matrices and quantum channels, respectively.

The category has as objects natural numbers. Morphisms $f : m \to n$ are $n \times m$ matrices. Composition is given by matrix multiplication: $(g \circ f)_i^j := \sum_k f_i^k g_k^j$, and the tensor is given by $m \otimes n := mn$ and $f \otimes g$ is the Kronecker product of matrices:

\[ (f \otimes g)_{ij}^{kl} := f_i^k g_j^l \vspace{-0pt}\]

Consequently, the tensor unit $I$ is the natural number $1$, so that states are column vectors $\rho : 1 \to n$, effects are row vectors $\pi : n \to 1$, and scalars are positive numbers $\lambda \in \mathbb R_+$.

is compact closed with $n = n^*$, where cups and caps are given by the Kronecker delta, $\delta_{ij}$, $\delta_{ij} = 1$ if $i = j$, $\delta_{ij} = 0$ otherwise. That is:

\[ \eta^{ij} := \delta_{ij} =: \epsilon_{ij} \vspace{-0pt}\]

The category has as objects the sets of linear operators, $\mathcal L(H)$, $\mathcal L(K), \ldots$, on finite dimensional Hilbert spaces $H,K,\ldots$ and morphisms $\Phi: \mathcal L(H) \to \mathcal L(K)$ are completely positive maps (i.e., positive maps which are still positive when tensored with other maps) with the usual composition: $\Phi \circ \Psi (a) = \Phi(\Psi(a))$.

The tensor product on objects satisfies $\mathcal L(H) \otimes \mathcal L(K) \cong \mathcal L(H \otimes K)$, and on morphisms it is given by linear extension of $\Phi \otimes \Psi (a \otimes b) = \Phi(a) \otimes \Psi(b)$.
Consequently, the tensor unit is $I = \mathcal L (\mathbb C) \cong \mathbb C$ and a state is a (completely) positive map $\rho:\mathbb C \to \mathcal L(H)$. Identifying such a map with its image on 1, we may say that a state is positive operator in $\mathcal L (H)$.
Effects are (un-normalised) quantum effects, i.e., (completely) positive maps $\pi: \mathcal L (H) \to \mathbb C$, and are of the form: $\pi(a) := \textrm{Tr}(P a)$, for some positive operator $P$. As with , the scalars are $\mathbb R_+$.

is also compact closed, with cups and caps given by the (un-normalised) Bell state:

\[ \eta = \ketbra{\Phi_0}{\Phi_0} \qquad \epsilon(\rho) = \textrm{Tr}(\rho \ketbra{\Phi_0}{\Phi_0})\]

where $\ket{\Phi_0} = \sum_i \ket{i} \otimes \ket{i}$. Consequentially, $\mathcal L(H)^* = \mathcal L(H)$ and equation (<ref>) gives the basis-dependent version, i.e., `Choi-style', of the Choi-Jamiołkowski isomorphism [28].

§.§ $*$-autonomous categories

The biggest convenience of a compact closed structure is also its biggest drawback:

all higher-order structure collapses to first-order structure! For example, if we (temporarily) take $A \limp B := A^* \otimes B$ to be the object whose states correspond to processes from $A$ to $B$, we have:

\begin{align*}
(A \limp B) \limp C
& := (A \limp B)^* \otimes C \\
& := (A^* \otimes B)^* \otimes C \\
& \cong A^{**} \otimes B^* \otimes C \\
& \cong A \otimes B^* \otimes C \\
& \cong B^* \otimes A \otimes C \\
& =: B \limp A \otimes C
\end{align*}

As we will soon see, there is a pronounced difference between first-order causal processes which we introduce in the next section, and genuinely higher-order causal processes (see Chapter <ref>). Hence, we would not expect such a collapse. If we look carefully at the calculation above, we see that things went wrong in the third step above. Because in any compact closed category, we always have $(A \otimes B)^* \cong A^* \otimes B^*$, we are able to distribute $(-)^*$ over $\otimes$. If we remove this condition, we obtain a new, weaker kind of category:

A $*$-autonomous category is a symmetric monoidal category equipped with a full and faithful functor $(-)^* : \mathcal C^{\textrm{op}} \to \mathcal C$ such that, by letting:

\begin{equation}\label{eq:limp-def}
A \limp B := (A \otimes B^*)^*\vspace{-0pt}
\end{equation}

there exists a natural isomorphism:

\begin{equation}\label{eq:closure}
\mathcal C(A \otimes B, C) \cong \mathcal C(A, B \limp C)\vspace{-0pt}
\end{equation}

As the notation and the isomorphism (<ref>) suggest, $A \limp B$ is the system whose states correspond to processes from $A$ to $B$.
Indeed, take $A = I$ in (<ref>).

Note that the definition we gave for $A \limp B$ differs from the one we gave for compact closed categories. Indeed any compact closed category is $*$-autonomous, where it additionally holds that:

\begin{equation}\label{eq:star-dist}
A \otimes B \cong (A^* \otimes B^*)^*\vspace{-0pt}
\end{equation}

in which case:

\[ A \limp B := (A \otimes B^*)^* \cong A^* \otimes B^{**} \cong A^* \otimes B\vspace{-0pt} \]

However, in a $*$-autonomous category, the RHS of (<ref>) is not $A \otimes B$, but something new, called the `par' of $A$ and $B$:

\begin{equation}\label{eq:par-dual}
A \parr B := (A^* \otimes B^*)^*\vspace{-0pt}
\end{equation}

This new operation inherits its good behaviour from $\otimes$:

\[ A \parr (B \parr C) \cong (A \parr B) \parr C \qquad\qquad A \parr B \cong B \parr A \vspace{-0pt}\]

So a compact closed category is just a $*$-autonomous category where $\otimes = \parr$. However, this little tweak yields a much richer structure of higher-order maps.
We think of $A \otimes B$ as the joint state space of $A$ and $B$,

whereas $A \parr B$ is like taking the space of maps from $A^*$ to $B$.

For (first order) state spaces, these are basically the same, but as we go to higher order spaces, $A \parr B$ tends to be much bigger than $A \otimes B$.

We adopt the programmers' convention that $\otimes$ has precedence over $\limp$ and that $\limp$ associates to the right:

\[
A \otimes B \limp C := (A \otimes B) \limp C
\quad \quad A \limp B \limp C := A \limp (B \limp C)\vspace{-0pt}
\]

Either expression above represents the system whose states are processes with two inputs. Indeed (<ref>) implies that $A \otimes B \limp C \cong A \limp B \limp C$. Since $\mathcal C$ is symmetric, we can re-arrange the inputs at will, i.e.,

\begin{equation}\label{eq:lolli-sym}
A \limp B \limp C \cong B \limp A \limp C\vspace{-0pt}
\end{equation}

§.§ Discarding, causality, and non-signalling

As noted in [12, 14, 15, 7], the crucial ingredient for defining causality is a preferred discarding process $\disc_{\!\!A}$ from every system $A$ into $I$, which is compatible with the monoidal structure, in that

\begin{equation}\label{eq:discarding-eqs}
\discard_{\!\!A \otimes B} \ :=\  \discard_{\!\!A}\ \discard_{\!\!B}
\qquad
\discard_{\!\!I} \ :=\  1
\end{equation}

Using this effect, we can define causality as follows:

For systems $A$ and $B$ with discarding processes, a process $\Phi : A \to B$ is said to be causal if:

\begin{equation}\label{eq:causal}
\tikzfig{causal}
\end{equation}

Intuitively, causality means that if we disregard the output of a process, it does not matter which process occurred.

Hence causal states
produce $1$ when discarded:

\[ \pointmap{\rho}\ \ \textit{causal} \ \ \iff \ \ \weight{\rho}\ =\ 1 \]

Since discarding the `output' of an effect $\pi : A \to I$ is the identity, there is a unique causal effect for any system, namely discarding itself:

\[ \copointmap{\pi}\ \ \textit{causal} \ \ \iff \ \ \copointmap{\pi}\ =\ \discard \]

For , the discarding process is a row vector consisting entirely of $1$'s; it sends a state to the sum over its vector entries:

\[ \discard\ =\ \left(\begin{matrix}
1 & 1 & \cdots & 1
\end{matrix}\right) \qquad \qquad
\weight{\rho} \ =\ \sum_i\ \rho^i \]

So, causality is precisely the statement that a vector of positive numbers sums to $1$, i.e., forms a probability distribution. Consequentially, the causality equation (<ref>) for a process $\Phi$ states that each column of $\Phi$ must sum to $1$. That is, $\Phi$ is a stochastic map.

For , discard is the trace. Hence causal states are positive operators with unit trace a.k.a. density operators  and causal processes are trace-preserving completely positive maps, a.k.a. quantum channels.

Discarding not only allows us to express when a process is causal,
it also allows us to represent causal relationships between the systems involved.

For example

A causal process $\Phi: A \otimes B \to A' \otimes B'$ is one-way signalling with $\evt{A}$ before $\evt{B}$ (written $\evt{A} \preceq \evt{B}$ where $\evt A := (A, A')$ and $\evt B := (B, B')$)
if there exists a process $\Phi':A \to A'$ such that

\begin{equation}\label{eq:a-before-b}
\tikzfig{NSBtoA}
\end{equation}

It is one-way signalling with $\evt{B} \preceq \evt{A}$ if there exists $\Phi''$ such that

\begin{equation}\label{eq:b-before-a}
\tikzfig{NSAtoB}
\end{equation}

Such a process is called non-signalling
if it is both one-way signalling with $\evt{A} \preceq \evt{B}$ and $\evt{B} \preceq \evt{A}$.

At first, this might seem like curious terminology, since non-signalling processes are a special case of one-way signalling processes. This is because the term `one-way signalling' does not imply that there is communication from Alice to Bob, but rather that communication is only allowed from Alice to Bob (and not from Bob to Alice). Contrast this with arbitrary causal processes $\Phi: A \otimes B \to A' \otimes B'$, which allow two-way communication in general.

Note that the expressions $\evt A \preceq \evt B$ and $\evt B \preceq \evt A$ in Definition <ref> are not written in terms of individual inputs or outputs of $\Phi$, but rather input/output pairs $\evt A := (A, A')$ and $\evt B := (B, B')$.
We call such an input/output pair from a given process an event.
If we think of an event in operational terms, it corresponds to a single agent giving an input to his or her black box (e.g., making a measurement choice) and then reading the output.

The definition of one-way signalling readily generalises from two events to $n$ events:

A process $\Phi$
is one-way signalling with $\evt{A}_1 \preceq \ldots \preceq \evt{A}_{n-1} \preceq \evt{A}_n$ if
with $\Phi'$ one-way signalling with $\evt{A}_1 \preceq \ldots \preceq \evt{A}_{n-1}$.

Intuitively, this captures that fact that $\Phi$ is consistent with the linear causal ordering of events $\evt A_i = (A_i, A_i')$. Following [25], we can extend this from linear causal orderings to arbitrary (acyclic) causal orderings. For a process $\Phi : A_1 \otimes \ldots \otimes A_n \to A_1' \otimes \ldots \otimes A_n'$, let $\mathcal O$ be a partially ordered set whose elements are the pairs $\{ \evt A_i := (A_i, A_i') \}_{1 \leq i \leq n}$, which we call a causal ordering for $\Phi$. Then, for any subset of events $\mathcal E \subseteq \mathcal O$ let $\past(\mathcal E)$ be the down-closure of $\mathcal E$ with respect to the ordering $\preceq$ of $\mathcal O$, i.e.,

\[ \past(\mathcal E) := \{ e \ |\ \exists e' \in \mathcal E\,.\, e \preceq e' \} \]

In particular, this set contains $\mathcal E$ itself. Furthermore, let $\pi_1(\mathcal E)$ and $\pi_2(\mathcal E)$ be given as the direct images of the first and second projections, namely all of the inputs in $\mathcal E$ and all the outputs in $\mathcal E$, respectively.

A process $\Phi : A_1 \otimes \ldots \otimes A_n \to A_1' \otimes \ldots \otimes A_n'$ is consistent with a causal ordering $\mathcal O$ (written $\Phi \vDash \mathcal O$) if for all subsets $\mathcal E \subseteq \mathcal O$, the outputs of $\mathcal E$ only depend on the inputs of $\past(\mathcal E)$. That is, there exists another process $\Phi'$ such that:

\begin{equation}\label{eq:causal-ord}
\tikzfig{satisfies}
\end{equation}

Note that, for clarity, we have suppressed the symmetry morphisms (i.e., swap maps) re-ordering the inputs and outputs of $\Phi$ in (<ref>). In particular, this equation should be understood to apply to all sets of inputs $\pi_1(\past(\mathcal E))$ and outputs $\pi_2(\mathcal E)$, not just the leftmost ones.

Definition <ref> is most easily understood by means of an example. Consider the following process with 5 inputs and outputs:
and the following causal ordering on input/output pairs of $\Phi$:

\[
\mathcal O := \left\{
\ \tikzfig{causal-graph}\
\right\}
\qquad \textrm{where} \qquad
\begin{cases}
\evt{A} := \text{\footnotesize $(A,A')$} \\
\evt{B} := \text{\footnotesize $(B,B')$} \\
\evt{C} := \text{\footnotesize $(C,C')$} \\
\evt{D} := \text{\footnotesize $(D,D')$} \\
\evt{E} := \text{\footnotesize $(E,E')$}
\end{cases}
\]

where the ordering is depicted from bottom-to-top, e.g., $\evt{A} \preceq \evt{B}$. Then, $\Phi \vDash \mathcal O$ if for all $\mathcal E \subseteq \mathcal O$, (<ref>) is satisfied. For example, taking $\mathcal E := \{ \evt{B} \}$, we have $\past(\{\evt{B}\}) = \{ \evt{A}, \evt{B}, \evt{C} \}$. So, condition (<ref>) requires that there exists $\Phi' : A \otimes B \otimes C \to B'$ such that:

Definition <ref> generalises the other (non)signalling conditions given before. For example, one-way signalling $\evt{A} \preceq \evt{B}$ and $\evt{B} \preceq \evt{A}$ can be stated respectively as:

\[
\tikzfig{bi-channel} \ \vDash \tikzfig{causal-graph-AB}
\qquad\textrm{and}\qquad
\tikzfig{bi-channel} \ \vDash \tikzfig{causal-graph-BA}
\]

whereas non-signalling is equivalent to the following:

\[
\tikzfig{bi-channel} \ \vDash \tikzfig{causal-graph-ns}
\]

There is a close connection between causality (<ref>) and consistency with a causal ordering $\mathcal O$. Namely, any (acyclic) string diagram has an evident causal ordering on the inputs/outputs of each of the component boxes, where $\evt{A} \preceq \evt{B}$ if and only if there is a forward-directed path from the box with inputs/outputs $(A,A')$ to the box with inputs/outputs $(B,B')$. For example:

\[
\tikzfig{caus-circ}
\qquad\qquad \textrm{\large$\leadsto$} \qquad\qquad
\tikzfig{causal-graph-2}
\]

It was shown in [25] that all acyclic diagrams in a category $\mathcal C$ respect their associated causal ordering if and only if all processes in $\mathcal C$ satisfy the causality equation (<ref>).

In the coming sections, we will show that consistency with a causal ordering can be expressed within the logic of a higher-order causal category. As a consequence, higher-order constraints such as preserving processes which are consistent with a causal ordering can also be expressed.

§ PRECAUSAL CATEGORIES

Precausal categories give a universe of all processes, and provide enough structure for us to identify which of those processes satisfy first-order and higher-order causality constraints. They are defined as compact closed categories satisfying four extra axioms, which involve discarding and its transpose:

\begin{equation}\label{eq:maxmix-unnorm}
\tikzfig{maxmix-disc}
\end{equation}

which we call the (unnormalised) uniform state.

A precausal category is a compact closed category $\mathcal C$ such that:

$\mathcal C$ has discarding processes for every system, compatible with the monoidal structure as in (<ref>).

For every (non-zero) system $A$, the dimension of $A$:

\[ d_A \ :=\  \tikzfig{dim} \]

is an invertible scalar.

$\mathcal C$ has enough causal states:

\[ \left(\textrm{\footnotesize $\forall \rho\ \textit{causal}\ .\ $}\tikzfig{causal-agree}\right)
\implies\ \  \tikzfig{causal-agree1} \]

Second-order causal processes factorise:

\[
\quant{\forall \Phi\ \textit{causal}}{\tikzfig{soc}}
\implies
\quant{\exists \Phi_1,\Phi_2\ \textit{causal}}{\tikzfig{soc-factor}}
\]

enables one to talk about causal processes within $\mathcal C$. enables us to renormalise certain processes to produce causal ones. For example, every non-zero system has at least one causal state, called the uniform state. It is obtained by normalising (<ref>):

Note that we allow $\mathcal C$ to have a zero object, in which case $d_0 = 0$ is not required to be invertible.

says that processes are characterised by their behaviour on causal states. Since $\mathcal C$ is compact closed, implies that it suffices to consider only product states to identify a process.

For any compact closed category $\mathcal C$, is equivalent to:

\begin{equation}\label{eq:enough-product-states}
\quant{\forall \rho_1, \rho_2 \ \textit{causal}}
\ \implies\
\tikzfig{remove-one1}
\end{equation}

follows from (<ref>) by taking one of the two systems involved to be trivial. Conversely, assume the premise of (<ref>). Applying one time yields:
for all causal states $\rho_2$. Bending the wire yields:
Hence we can apply a second time. Bending the wire back down gives the result.

is perhaps the least transparent. It says that the only mappings from causal processes to causal processes are `circuits with holes', i.e., those mappings which arise from plugging a causal process into a larger circuit of causal processes. This can equivalently be split into two smaller pieces, which may look more familiar to some readers.

For a compact closed category $\mathcal C$ satisfying , , and , condition is equivalent to the following two conditions:

Causal one-way signalling processes factorise:

\[ \quant{\exists\ \Phi'\ \textit{causal}}{\tikzfig{one-way-sig}}
\implies
\quant{\exists\ \Phi_1,\Phi_2\ \textit{causal}}{\tikzfig{one-way-sig2}}
\]

For all $w : A \otimes B^*$:

\[ \quant{\forall \Phi \ \textit{causal}}
{\tikzfig{causal-eff}\ =\ 1}
\implies
\quant{\exists \rho \ \textit{causal}}
{\tikzfig{causal-eff-splits}} \]

Assume holds, and let $\Phi$ satisfy the premise of . Then, for causal $\Psi$, we have:
Hence, by there exist causal $\Phi_1', \Phi_2$ such that:
Deforming then gives the factorisation in .

To get to from , we take the input and output systems of $w$ trivial, which gives:
where the second `$=$' follows from the fact that discarding is the unique causal effect.

Conversely, suppose and hold. Let $w$ be a second order causal process. Then, for any causal $\rho$ and $\Phi$:

\[ \tikzfig{causal-eff-splits1}\ =\ 1 \]

So, by :
Then, by :
Hence $w$ satisfies the premise of , up to diagram deformation, where $\Phi := w$ and $\Phi' := w'$, which implies that it factors as in .

For any $w : A \otimes B^*$:

\[
\lquant{\exists \rho}{\tikzfig{causal-eff-splits}}
\ \iff\
\left(\ \tikzfig{SOC_splits_lemma-long}\ \right)
\]

$(\Leftarrow)$ immediately follows from diagram deformation. For $(\Rightarrow)$, assume the leftmost equation above. Then we can obtain an expression for $\rho$ by plugging the uniform state into $w$ and applying causality of the uniform state:
Substituting this expression back in for $\rho$ yields:

\[\tikzfig{rho-as-comb1} \]

and are both precausal categories. See appendix for proofs of conditions -.

, the category whose objects are sets and whose morphisms $R : X \to Y$ are relations $R \subseteq X \times Y$ with $R \otimes S := R \times S$, is not a pre-causal category. Nevertheless, it satifies axioms -and , so it could be called a weakly pre-causal category. See appendix for proofs and a counter-example of .

We now show that implies a general $n$-fold version of itself:

Let $\Phi$ be one-way signalling with $\evt A_1 \preceq \ldots \preceq \evt A_n$, then there exists $\Phi_1,\ldots, \Phi_n$ such that

For $n=2$, this is just .
Suppose the proposition is true for $n-1$.
Then because
for some one way signalling process $\Phi'$ with $\evt A_1 \preceq \ldots \preceq \evt A_{n-1}$,
we have by that there exists $\Phi'_{n-1}$ and $\Phi_n$ such that
It follows that $\Phi'$ equals $\Phi'_{n-1}$ with the $C$ system discarded,
so that $\Phi'_{n-1}: A_1 \otimes \ldots \otimes A_{n-1} \to A'_1 \otimes \ldots \otimes (A'_{n-1} \otimes C)$ is again one-way signalling.

By assumption $\Phi'_{n-1}$ now factors and hence so does $\Phi$.

While, as we shall soon see, precausal categories give us a source of processes exhibiting many varieties of definite and indefinite causal structure, the axioms rule out certain, paradoxical causal structures. To see this, we state our first no-go result for a precausal category $\mathcal C$.

No non-trivial system $A$ in a precausal category $\mathcal C$ admits time travel.
That is, if there exist systems $B$ and $C$ such that for all processes $\Phi$ we have:

\begin{equation}\label{eq:time-travel}
\tikzfig{time-phi}\  \textit{causal} \qquad \implies \qquad \tikzfig{time-travel}\ \textit{causal}\vspace{-0pt}
\end{equation}

then $A \cong I$.

For any causal process $\Psi : A \to A$, we can define:

which is also a causal process. Then implication (<ref>) gives:

\[ \tikzfig{time-travel1} \vspace{-0pt}\]

Applying $\Cf$, we have:

\[ \tikzfig{time-travel3} \qquad \implies \qquad \tikzfig{time-travel4} \]

for some causal state $\rho : I \to A$. That is, $\rho \circ \disc = 1_A$, and by definition of causality for $\rho$, $\disc \circ \rho = 1_I$.

Note that a special case of Theorem <ref> implies that if for all causal processes $\Phi : A \to A$ we have
then $A \cong I$.

§ CONSTRUCTING

We will now describe our main construction, the category $\CausC$ of higher-order causal processes for a precausal category $\mathcal C$. To motivate this construction, we begin by looking at the properties of the set of causal states for some system $A$:

\begin{equation}\label{eq:all-causal-states}
\left\{ \rho : A \ \bigg|\ \weight{\rho} \ =\ 1 \right\} \subseteq \mathcal C(I, A)
\end{equation}

In the classical and quantum cases, these form convex subsets of real vector spaces (probability distributions in $\mathbb R^n$ and density matrices in $\textrm{SA}_n$, the self adjoint $n \times n$ operators, respectively). We would like to recapture the fact that this set is suitably closed without referring to convexity, so we appeal to duals instead.

For any set of states $c \subseteq \mathcal C(I, A)$, we can define the dual set $c^* \subseteq \mathcal C(I, A^*)$ as follows:

\[ c^*\ :=\ \left\{ \pi : A^* \ \bigg|\ \forall \rho \in c\ .\ \unbig{\pointbraket{\rho}{\pi}} \ =\ 1 \right\} \]

Taking the dual again, we get back to a set of states in $A$. It immediately follows from the definition that $c \subseteq c^{**}$. For the set of all causal states (<ref>), we see that furthermore $c = c^{**}$.

A set of states $c \subseteq \mathcal C(I, A)$ is closed if $c = c^{**}$ and flat if there exist invertible scalars $\lambda, \mu$ such that:

\[ \lambda\ \maxmix\ \in c \qquad\qquad \mu\ \discard \in c^* \]

For a precausal category $\mathcal C$, the category $\CausC$ has as objects pairs:

\[\bm A := (A, c_{\bm A} \subseteq \mathcal C(I, A))\vspace{-0pt} \]

where $c_{\bm A}$ is closed and flat. A morphism $f : \bm A \to \bm B$ is a morphism $f : A \to B$ in $\mathcal C$ such that:

\begin{equation}\label{eq:caus-condition}
\rho \in c_{\bm A}\ \implies\ f \circ \rho \in c_{\bm B}\vspace{-0pt}
\end{equation}

We refer to categories of the form $\Caus[\mathcal C]$ for some precausal category $\mathcal C$ as higher-order causal categories (HOCCs).

While condition (<ref>) is given in terms of states, closure allows us to equivalently present it in terms of effects or numbers:

For objects $\bm A, \bm B$ in $\CausC$ and a morphism $f : A \to B$ in $\mathcal C$, the following are equivalent:

(i) $\rho \in c_{\bm A} \implies f \circ \rho \in c_{\bm B}$

(ii) $\pi \in c_{\bm B}^* \implies \pi \circ f \in c_{\bm A}^*$

(iii) $\rho \in c_{\bm A}, \pi \in c_{\bm B}^* \implies \pi \circ f \circ \rho = 1$

(i) $\Rightarrow$ (ii) and (ii) $\Rightarrow$ (iii) follow immediately from the definition of $(-)^*$, so assume (iii) and take any $\rho \in c_{\bm A}$. Then for all $\pi \in c_{\bm B}^*$, $\pi \circ (f \circ \rho) = 1$. Hence $f \circ \rho \in c_{\bm B}^{**} = c_{\bm B}$.

Since a set of states is closed when $c = c^{**}$, it is natural to ask if $(-)^{**}$ forms a closure operation, namely if it is idempotent. This is an immediate result of the following:

For any set of states $c$ we have $c^{*} = c^{***}$.

First, note that:

\[ c \subseteq d \ \implies \ d^* \subseteq c^*. \]

Applying this to $c \subseteq c^{**}$ yields $c^{***} \subseteq c^*$.
But then, it is already the case that $c^*$ is contained in $c^{***}$,
so $c^{***} = c^*$.

We will now show that $\CausC$ has the structure of a $*$-autonomous category. To do this, we will first define the tensor $\bm A \otimes \bm B$. For the sets of states $c_{\bm A}$ and $c_{\bm B}$, we denote the set of all product states as follows:

\[ c_{\bm A} \otimes c_{\bm B} \ :=\ \{ \rho_1 \otimes \rho_2 \ |\ \rho_1 \in c_{\bm A},\ \rho_2 \in c_{\bm B} \}\vspace{-0pt} \]

Then, $c_{\bm A \otimes \bm B}$ is the closure of the set of all product states:

\[ c_{\bm A \otimes \bm B} := (c_{\bm A} \otimes c_{\bm B})^{**}\vspace{-0pt} \]

For any effect $\pi : A^* \otimes B^*$ in $\mathcal C$:

\begin{equation}\label{eq:tensor-effects}
\quant{\forall\ \rho \in c_{\bm A \otimes \bm B}}
{\tikzfig{bi-braket1}\ =\ 1}
\ \ \iff\ \
\quant{\forall\ \rho_1 \in c_{\bm A}, \rho_2 \in c_{\bm B}}
{\tikzfig{bi-braket2}\ =\ 1}
\end{equation}

The LHS of (<ref>) states that

\[ \pi \in c_{\bm A \otimes \bm B}^* := ((c_{\bm A} \otimes c_{\bm B})^{**})^* = (c_{\bm A} \otimes c_{\bm B})^{***} \vspace{-0pt}\]

whereas the RHS states that $\pi \in (c_{\bm A} \otimes c_{\bm B})^{*}$. Hence, (<ref>) follows from Lemma <ref>.

$\CausC$ is an SMC, with tensor given by:

\[ \bm A \otimes \bm B := (A \otimes B, c_{\bm A \otimes \bm B})\vspace{-0pt} \]

and tensor unit $\bm I := (I, \{1\})$.

The proof is in the appendix.

Now define objects $\bm A^* := (A^*, c_{\bm A^*})$ in the obvious way, by letting $c_{\bm A^*} := c_{\bm A}^*$. Then

The transposition functor $(-)^* : \mathcal C^{\textrm{op}} \to \mathcal C$:

\begin{equation}\label{eq:trans-functor}
A\mapsto A^* \qquad\qquad \tikzfig{transpose}
\end{equation}

lifts to a full and faithful functor $(-)^* : \CausC^{\textrm{op}} \to \CausC$, where $\bm A^* := (A^*, c_{\bm A^*})$.

The main part is showing that $f^*$ is again a morphism, but this follows from the definition of the star on sets of states.
A full proof is in the appendix.

We now have enough structure to define $\bm A \limp \bm B := (\bm A \otimes \bm B^*)^*$. However, it is enlightening to give an explicit characterisation of the set $c_{\bm A \limp \bm B}$. This will be no surprise:

For objects $\bm A, \bm B \in \CausC$:

\[ c_{\bm A \limp \bm B} = \left\{ f : A^* \otimes B\ \bigg|\ \forall \rho \in c_{\bm A}, \pi \in c_{\bm B}^*\ .\ \tikzfig{dual-f1}\ =\ 1 \right\} \]

This follows by simplifying:

\[
c_{(\bm A \otimes \bm B^*)^*}
= c_{(\bm A \otimes \bm B^*)}^*
= (c_{\bm A} \otimes c_{\bm B^*})^{***}
= (c_{\bm A} \otimes c_{\bm B}^*)^{*}
\]

and noting that $f \in (c_{\bm A} \otimes c_{\bm B}^*)^{*}$ is precisely the statement given in the lemma.

For any precausal category $\mathcal C$, is a $*$-autonomous category where $\bm I = \bm I^*$.

Since compact closed categories already admit an interpretation for $\limp$ satisfying (<ref>), it suffices to show that this isomorphism lifts to . This follows from the application of Lemma <ref>. The complete proof is in the appendix.

Since is $*$-autonomous, we can also define the `par' of two systems $\bm A \parr \bm B$. Since $\parr$ is related to $\limp$ via $\bm A \parr \bm B \cong \bm A^* \limp \bm B$, Lemma <ref> also yields an explicit form for $c_{\bm A \parr \bm B}$ by replacing $\bm A$ with $\bm A^*$:

\[
c_{\bm A \parr \bm B} =
\left\{ \rho : A \otimes B\ \bigg|\ \textrm{\footnotesize$\forall \pi \in c_{\bm A}^*, \xi \in c_{\bm B}^*\ .\ $}\tikzfig{par} = 1 \right\} \]

Note that the process $f : A^* \otimes B$ has become a bipartite state $\rho : A \otimes B$. That is, the states $\rho : \bm A \parr \bm B$ are states which are normalised for all product effects. Symbolically, the two monoidal products are defined as follows:

\[
c_{\bm A \otimes \bm B} = (c_{\bm A} \otimes c_{\bm B})^{**}
\qquad
c_{\bm A \parr \bm B} = (c_{\bm A}^* \otimes c_{\bm B}^*)^*\vspace{-0pt}
\]

One can easily check that $(c_{\bm A}^* \otimes c_{\bm B}^*) \subseteq (c_{\bm A} \otimes c_{\bm B})^*$. Thus, since $(-)^*$ reverses subset inclusions, that
$c_{\bm A \otimes \bm B} \subseteq c_{\bm A \parr \bm B}$.
Consequently, the identity $1_{A \otimes B}$ in $\mathcal C$ lifts to a canonical embedding $\bm A \otimes \bm B \hookrightarrow \bm A \parr \bm B$ in . This agrees with the intuition given in Section <ref> that $\bm A \parr \bm B$ is the `larger' of the two ways to combine $A$ and $B$ into a joint system.

A $*$-autonomous category with coherent isomorphism $I \cong I^*$, such as , is also called an ISOMIX category [10]. This innocent-looking extra condition actually gives a great deal more structure. For instance, even though we showed it concretely, the existence of a canonical morphism $A \otimes B \to A \parr B$ is implied purely from this extra structure.

Rather than thinking of as a totally new category constructed from $\mathcal C$, it is useful to think of it as endowing the processes in $\mathcal C$ with a much richer type system. As in the compact closed case, it suffices to consider only processes out of $\bm I$ and we use $\rho : \bm X$ as shorthand for $\rho : \bm I \to \bm X$. However, unlike before, we will often use a statement of the form $\rho : \bm X$ as a proposition about a state $\rho \in \mathcal C(I, X)$.

For a system $\bm X = (X, c_{\bm X})$ in and a state $\rho \in \mathcal C(I, X)$, $\rho : \bm X$ if and only if $\rho \in c_{\bm X}$.

Since $1$ is the unique state in $c_{\bm I}$, the result follows immediately from the definition of morphism in :

\[ \rho : \bm X \ \iff\  \rho \circ 1 \in c_{\bm X} \ \iff\ \rho \in c_{\bm X} \]

From now on, we will use $\rho : \bm X$ and $\rho \in c_{\bm X}$ interchangeably without further comment. We will also mix the graphical notation with the type-theoretic. So, for instance, if we write:

\[
\tikzfig{composition}\ \ :\ \bm A \limp (\bm B \limp \bm C) \limp \bm D\vspace{-0pt}
\]

this should be interpreted as a morphism in $\mathcal C(I, A^* \otimes B \otimes C^* \otimes D)$, along with the assertion that this morphism has type $\bm A \limp (\bm B \limp \bm C) \limp \bm D$. In particular, diagrams always depict $\mathcal C$-morphisms, as opposed to -morphisms, so there is no ambiguity about whether parallel composition means $\otimes$ or $\parr$.

Furthermore, if we state that two types are isomorphic without giving the isomorphism explicitly, it should be understood that the underlying isomorphism in $\mathcal C$ is just the identity, up to a possible permutation of systems. In particular, $\bm X \cong \bm Y$ implies that $\rho : \bm X$ if and only if $\rho : \bm Y$.

§ FIRST ORDER SYSTEMS

For any precausal category $\mathcal C$, we can always form the SMC of (first-order) causal processes $\mathcal C_c$ by restricting just to those processes satisfying the causality equation (<ref>). Since is supposed to contain first and higher-order causal processes, one would naturally expect $\mathcal C_c$ to embed in .

A system $\bm A = (A, c_{\bm A})$ in $\CausC$ is called first order if it is of the form $(A, \{ \disc_{\!\!A} \}^*)$.

Note that $\{ \disc_{\!\!A} \}^*$ is precisely the set (<ref>) of causal states of type $A$. Clearly this set is flat and closed. Indeed, this was the motivation for these conditions in the first place. Now, we show that the processes between first-order systems in are exactly as expected.

Let $\bm A, \bm B$ be first-order systems. Then $f$ is a morphism from $\bm A$ to $\bm B$ if and only if it is causal.

We first compute $c_{\bm A}^*$ for a first-order system. Suppose $\pi \in c_{\bm A}^*$. Then for all causal states $\rho$, $\pi \circ \rho = 1 = \disc_{\!\!A} \circ \rho$, so by $\pi = \disc_{\!\!A}$. Hence $c_{\bm A}^* = \{ \disc_{\!\!A} \}$.

Now, by Proposition <ref>, $\Phi \in \mathcal C(A, B)$ is a morphism from $\bm A$ to $\bm B$ if and only if for every $\pi \in c_{\bm B}^*$, $\pi \circ \Phi \in c_{\bm A}^*$. Since both of these sets of effects only contain discarding, this reduces to the causality equation (<ref>).

Furthermore, first-order systems are closed under $\otimes$.

For first order systems $\bm A$, $\bm B$, $\bm A \otimes \bm B$ is also a first-order system, given by:

\[ \bm A \otimes \bm B = (A \otimes B, \{ \disc_{\!\!A} \disc_{\!\!B} \}^*)\vspace{-0pt} \]

It suffices to show that $c_{\bm A \otimes \bm B}^* = \{ \disc_{\!\!A} \disc_{\!\!B} \}$. Let $\pi \in c_{\bm A \otimes \bm B}^*$, then for all causal states $\rho_1 \in c_{\bm A}, \rho_2 \in c_{\bm B}$:

\[ \tikzfig{bi-braket2}\ =\ 1 \]

Hence, by Proposition <ref>, $\pi = \disc_{\!\!A} \disc_{\!\!B}$.

There exists a full, faithful, monoidal embedding of the category $\mathcal C_c$ of causal processes into via:

\[ A \mapsto (A,\{\disc_{\!\!A}\}^*) \qquad\qquad f \mapsto f \vspace{-0pt}\]

Hence, the full sub-category of first-order systems and processes behaves as expected; it is equivalent to $\mathcal C_c$. Perhaps a more surprising corollary to Proposition <ref> is the following.

Let $\bm A$ and $\bm B$ be first order systems, then:

\[ \bm A \otimes \bm B \cong \bm A \parr \bm B \vspace{-0pt}\]

$c_{\bm A \parr \bm B} := (c_{\bm A}^* \otimes c_{\bm B}^*)^* = \{ \disc_{\!\!A} \disc_{\!\!B} \}^* = c_{\bm A \otimes \bm B}$.

So for first-order systems, there is really only one way to form the `joint system'. However, we will now see that for higher-order systems, this is very much not the case.

§ HIGHER-ORDER SYSTEMS WITH DEFINITE CAUSAL ORDER

While it is important that the category of causal processes embeds fully and faithfully in when one restricts to first-order systems, the chief interest of are its higher-order systems.
The goal of this section is to show that certain collections of maps fit nicely within the developed type theory.

The first non-trivial second-order system that it is natural to consider is $\bm A \limp \bm B$ for first-order systems $\bm A$, $\bm B$. The isomorphism (<ref>) for $*$-autonomous categories restricts to:

\[ \CausC(\bm A, \bm B) \cong \CausC(\bm I, \bm A \limp \bm B) \vspace{-0pt}\]

so `states' $\Phi : \bm A \limp \bm B$ are in bijective correspondence with morphisms from $\bm A$ to $\bm B$ in . That is, they are precisely the causal processes from $\bm A$ to $\bm B$.

Now, starting from first-order systems $\bm A, \bm A', \bm B, \bm B'$, we have two ways to form the `joint system' from $\bm A \limp \bm A'$ and $\bm B \limp \bm B'$, via $\otimes$ and $\parr$. Before we characterise these systems, we examine the dual of a second-order system.

If we take a process $w: (\bm A \limp \bm B)^*$ in the dual system, we know from that that $w$ must split into two pieces, a causal state and the discard map. In fact, using flatness, we can strengthen this condition by only requiring $\bm B$ to be first-order.

For any system $\bm X$, first-order system $\bm B$, and process $w : (\bm X \limp \bm B)^*$, there exists $\rho : \bm X$ such that:

\begin{equation}\label{eq:ho-splitting}
\tikzfig{ho-causal-eff-splits-types}
\end{equation}

Since $\bm B$ is first-order, $c_{\bm B}^* = \{\disc_{\!\!B}\}$ and by flatness, for some $\mu$, $\mu \disc_{\!\!X} \in c^*_{\bm X}$. Hence, for any (first-order) causal process $\Phi : X \to B$, we have $\disc_{\!\!B} \circ \mu \Phi = \mu\ \disc_{\!X}$. Hence $\mu \Phi$ is of type $\bm X \to \bm B$. It follows by definition of $(\bm X \limp \bm B)^*$ that:

That is, $\mu w$ sends every causal process $\Phi$ to $1$, so by $\Cf$:

\[ \left(\tikzfig{ho-causal-eff-splits}\right)
\quad\implies\quad
\left(\tikzfig{ho-causal-eff-splits1}\right)\vspace{-0pt}
\]

It is then straightforward to show that $\rho := \mu^{-1} \rho'$ is a state of $\bm X$, e.g., by plugging the uniform state for system $\bm B$ into both sides of the equation above.

Equivalently, by Lemma <ref>, $w : (\bm X \limp \bm A)^*$ implies:

\begin{equation}\label{eq:ho-splitting-explicit}
\tikzfig{SOC_splits_lemma}
\end{equation}

We now characterize the two ways to combine the spaces $\bm A \limp \bm A'$ and $\bm B \limp \bm B'$:

For first-order systems $\bm A, \bm A', \bm B, \bm B'$, a process $\Phi$ is of type $(\bm A \limp \bm A')\otimes (\bm B \limp \bm B')$ if and only if it is causal and non-signalling.

First assume that $\Phi : (\bm A \limp \bm A')\otimes (\bm B \limp \bm B')$. Then, since discarding $B'$ is causal, we can regard it as a morphism $\disc_{\!\!B'} : \bm B' \to \bm I$. Hence by functoriality of $\otimes$ and $\limp$, we have:

\[ \tikzfig{disc-A}\ \ :\ (\bm A \limp \bm A')\otimes (\bm B \limp \bm I) \vspace{-0pt}\]

Then we can transform to an equivalent type as follows:

\begin{align*}
(\bm A \limp \bm A') \otimes (\bm B \limp \bm I)
& \cong (\bm A \limp \bm A') \otimes \bm B^* \\
& \cong ((\bm A \limp \bm A')^* \parr \bm B)^* \\
& \cong ((\bm A \limp \bm A') \limp \bm B)^*\vspace{-0pt}
\end{align*}

Hence, by Lemma <ref>, $\Phi$ splits as $\disc_{\!\!B} : \bm B$ and $\Phi' : \bm A \limp \bm A'$. This gives exactly the first non-signalling equation:
The second equation is shown similarly, by plugging in $\disc_{\!\!A'}$.

Conversely, suppose that $\Phi$ is causal and non-signalling. Then it satisfies the two non-signalling equations in Definition <ref>. Hence by , it can be factored in two ways:
for causal processes $\Phi_i, \Psi_i$.

Now, take any effect $w: ((\bm A\multimap \bm A')\otimes (\bm B \multimap \bm B'))^* \cong (\bm B \multimap \bm B') \multimap (\bm A\multimap \bm A')^*$. For any causal state $\rho$,

\[ \tikzfig{phi2rho} \ \ :\ \bm B \limp \bm B' \]

Plugging this into one side of $w$ gives:

\[ \tikzfig{SOC2-state-splits0}\ \ :\ (\bm A\multimap \bm A')^* \]

Applying equation (<ref>) gives:
Hence by enough causal states we have
It then follows that
Therefore $\Phi : ((\bm A\multimap \bm A')\otimes (\bm B \multimap \bm B'))^{**} = (\bm A\multimap \bm A')\otimes (\bm B \multimap \bm B')$.

The proof above also generalises straightforwardly to show that a process is $n$-paritite non-signalling, i.e., for all $i$:
if and only if:

\[ \Phi : (\bm A_1 \limp \bm A_1') \otimes
(\bm A_2 \limp \bm A_2') \otimes
\ldots \otimes
(\bm A_n \limp \bm A_n')\vspace{-0pt} \]

For first-order systems $\bm A, \bm A', \bm B, \bm B'$, a process $\Phi$ is of type $(\bm A \limp \bm A') \parr (\bm B \limp \bm B')$ if and only if it is causal. That is:

\[ (\bm A \limp \bm A') \parr (\bm B \limp \bm B') \cong
\bm A \otimes \bm B \limp \bm A \otimes \bm B' \vspace{-0pt}\]

We rely on the relationship between $\limp$ and $\parr$:

\begin{align*}
(\bm A \limp \bm A') \parr (\bm B \limp \bm B')
& \cong \bm A^* \parr \bm A' \parr \bm B^* \parr \bm B' \\
& \cong \bm A^* \parr \bm B^* \parr \bm A' \parr \bm B' \\
& \cong (\bm A^* \parr \bm B^*)^* \limp \bm A' \parr \bm B' \\
& \cong \bm A \otimes \bm B \limp \bm A' \parr \bm B'\vspace{-0pt}
\end{align*}

Then, since $\bm A'$ and $\bm B'$ are first-order, $\bm A' \parr \bm B' \cong \bm A' \otimes \bm B'$, which completes the proof.

So $(\bm A \limp \bm A') \parr (\bm B \limp \bm B')$ forms the joint system consisting of all causal processes from $\bm A \otimes \bm B$ to $\bm A' \otimes \bm B'$, including the signalling ones, e.g.

\[
\tikzfig{swap}\ \ :\ (\bm A \limp \bm B) \parr (\bm B \limp \bm A)\vspace{-0pt}
\]

Hence, $\otimes$ and $\parr$ represent two extremes by which $\bm A \limp \bm A'$ and $\bm B \limp \bm B'$ can be combined, namely by requiring them to be non-signalling or imposing no non-signalling conditions. In the next section, we will see how to recover types for one-way signalling processes.

§.§ Linear causal orders via combs

For first order systems $\bm A, \bm A', \bm B, \bm B'$,
a process $w$ is one-way signalling ($\evt{A} \preceq \evt{B}$) if and only if:

\[
\tikzfig{bi-w}\ \ :\ \bm A \multimap (\bm A' \multimap \bm B) \multimap \bm B'\vspace{-0pt}
\]

Suppose $\Phi$ is $\evt A \preceq \evt B$. First, we deform $\Phi$ to put the two $A$-labelled systems below the two $B$-labelled systems:

\[ \tikzfig{bi-w} \ \ \mapsto\ \ \tikzfig{bi-phi2} \vspace{-0pt}\]

The one-way signalling equation (<ref>) then becomes:

\begin{equation}\label{eq:bi-w-ns}
\tikzfig{bi-phi-ns}\vspace{-0pt}
\end{equation}

Now, by (<ref>) we have:

\[ \bm A \limp (\bm A' \limp \bm B) \limp \bm B'
\cong (\bm A' \limp \bm B) \limp \bm A \limp \bm B' \vspace{-0pt}\]

So, for $w$ to be a member of the above type, it must send all causal processes $\Psi : \bm A' \multimap \bm B$ to causal processes. This immediately follows from (<ref>):

Conversely, if $w$ sends causal processes to causal processes, it factorises as in , which implies (<ref>):

\[ \tikzfig{bi-phi-ns2} \]

Hence, one-way signalling admits a more general class of processes than (two-way) non-signalling.

One can show the embedding of non-signalling processes into one-way signalling processes purely at the level of types by relying on the linear distributivity property of $*$-autonomous categories [11]. Namely, in any $*$-autonomous category, there exists a canonical mapping:

\[ (\bm A \parr \bm B) \otimes \bm C \to \bm A \parr (\bm B \otimes \bm C) \vspace{-0pt}\]

We can use this to construct an embedding of non-signalling processes into one-way signalling processes:

\begin{align*}
(\bm A \limp \bm A') \otimes (\bm B \limp \bm B')
& \cong (\bm A^* \parr \bm A') \otimes (\bm B^* \parr \bm B') \\
& \to \bm A^* \parr (\bm A' \otimes (\bm B^* \parr \bm B')) \\
& \to \bm A^* \parr (\bm A' \otimes \bm B^*) \parr \bm B' \\
& \cong \bm A \limp (\bm A' \limp \bm B) \limp \bm B'\vspace{-0pt}
\end{align*}

Following [33], we generalise from 2-party, one-way signalling processes to $n$-party processes by recursively defining a the type of $n$-combs.

The $n$-combs $C_n$ are defined by

* $C_0 = \bm I$,

* $C_{i+1} = \bm B_{-i} \multimap C_i \multimap \bm B_{i+1}$

A 1-comb has type $\bm B_0 \limp \bm I \limp \bm B_1 \cong \bm B_0 \multimap \bm B_1$, so it is just a causal process. For higher combs, the `$-i$' is employed to maintain the left-to-right order of indices. For example, a 3-comb has type:

\[ \tikzfig{3-comb-bigger} : \bm B_{-2} \limp (\bm B_{-1} \limp (\bm B_0 \limp \bm B_1) \limp \bm B_2) \limp \bm B_3 \vspace{-0pt}\]

When necessary, we rename $\bm A_i := \bm B_{2i - n - 1}$ and $\bm A_i' := \bm B_{2i - n}$ to obtain e.g.,

\[ \bm A_1 \limp (\bm A_1' \limp (\bm A_2 \limp \bm A_2') \limp \bm A_3) \limp \bm A_3' \vspace{-0pt}\]

This recursive definition carries the following intuition. If we think of an $n$ comb as a communication protocol with $n$ input/output steps, then an $(n+1)$-comb is an $(n+1)$ step communication protocol, namely something which takes an initial input, then runs an $n$-step communication protocol, and produces a final output. Hence, we can represent the overall process of two agents running a communication protocol by plugging together Alice's $n$-comb and Bob's $(n-1)$-comb:

\[ \tikzfig{n-comb-plug2}\ :\ \ \bm A_1 \limp \bm A'_n \vspace{-0pt}\]

We give an alternative characterisation for combs in , which will relate to one-way signalling processes.

For any $n$-comb $w : C_n$, discarding the output $\bm A'_n$ separates as follows, for some $w'$:

\begin{equation}\label{eq:n-comb-sep}
\tikzfig{n-sep}
\end{equation}

Plugging any causal state into the first input of $w$ and discarding the last output yields:

\[
\tikzfig{n-sep-lhs}\ \ :\ C_{n-1} \limp \bm I\vspace{-0pt}
\]

\begin{align*}
C_{n-1} \limp \bm I  \cong C_{n-1}^* &  \cong (\bm B_{-(n-2)} \limp C_{n-2} \limp \bm B_{n-1})^* \\
& \cong (\bm B_{-(n-2)} \otimes C_{n-2} \limp \bm B_{n-1})^*\vspace{-0pt}
\end{align*}

Hence by Lemma <ref>, in particular equation (<ref>), we obtain:
The result then follows from enough causal states.

Note that we haven't actually said that $w'$ is itself an $(n-1)$-comb. We will show this now.

$w$ is an $n$-comb, i.e., $w : C_n$, if and only if it separates as in equation (<ref>) for some $w' : C_{n-1}$.

By induction. For $n=1$ the theorem is true because a $0$-comb is always $\bm I$.
Suppose the theorem is true for $n$.
Let $w$ be an $(n+1)$-comb. We need to show that $w'$ is an $n$-comb.
So let $y$ be any $(n-1)$-comb. Then, if we form the process:

\begin{equation}\label{eq:ih-y}
\tikzfig{IndHyp-y}\vspace{-0pt}
\end{equation}

then clearly discarding the top output results in an $(n-1)$ comb (namely $y$) and a discard.
So by the induction hypotheses, (<ref>) is an $n$-comb. Therefore we have

where $(*)$ follows from the definition of $(n+1)$-comb and $(**)$ is Lemma <ref>. Hence $w'$ sends any $(n-1)$-comb to a causal map, so $w'$ is itself an $n$-comb.

Conversely, let $w'$ in equation (<ref>) be an $n$-comb, and take any $n$-comb $y$.
Then by the induction hypothesis, discarding the top output of $y$ separates as discarding and an $(n-1)$-comb $y'$. Hence:

so $w$ is an $(n+1)$-comb.

Hence, $n$-combs can be characterised inductively in exactly the same way as $n$-party one-way signalling processes. Since $1$-combs are just causal processes, the following is immediate.

For first order systems $\bm A_1, \bm A'_1, \ldots, \bm A_n, \bm A'_n$, a map $w:A_1 \otimes \ldots \otimes A_n \to A'_1 \otimes \ldots \otimes A'_n$ is one-way signalling ($\evt{A}_1 \preceq \ldots \preceq \evt{A}_n$) if and only if it is of type $\bm A_1 \multimap ( \bm A'_1 \multimap ( \ldots ) \multimap \bm A_n ) \multimap \bm A'_n$.
That is, it is an $n$-comb.

Stated in terms of consistency with causal orderings, as defined in section <ref>, the above corollary says that $\Phi : \bm A_1 \multimap ( \bm A'_1 \multimap ( \ldots ) \multimap \bm A_n ) \multimap \bm A'_n$ if any only if:

\[
\tikzfig{nfold}\ \vDash\ \tikzfig{lin-ord}
\]

Proposition <ref>, then generalises the characterisation theorem for quantum combs in [6] to for any precausal $\mathcal C$: an $n$-comb always factors as a sequence of `memory channels', i.e., a composition of causal processes of the form:

§.§ Directed acyclic causal orders via pullback

We now extend from types which express consistency with arbitrary, linear causal orderings to all acyclic causal orderings. To do so, we first give a new characterisation of the consistency relation $\Phi \vDash \mathcal O$ defined in section <ref> in terms of all of the total orders refining the partial order $\mathcal O$. Recall the following standard definition:

For a partial order $\mathcal O$, a totalisation $\mathcal O'$ is a total order with the same elements as $\mathcal O$ such that $e \preceq_{\mathcal O} e' \implies e \preceq_{\mathcal O'} e'$.

Totalisations are not unique. For example, a typical `common cause' ordering admits two possible totalisations:

\[
\tikzfig{common-cause}
\qquad
\textrm{\large $\leadsto$}
\qquad
\tikzfig{common-cause-lin1}
\qquad
\textrm{and}
\qquad
\tikzfig{common-cause-lin2}
\]

corresponding to imposing the (extraneous) causal orderings $\evt{B} \preceq \evt{C}$ or $\evt{C} \preceq \evt{B}$.
Its important to note that causal constraints come from the absence of edges in the Hasse diagrams (i.e., diagrams to visualize a partial order) above, rather than the presence. That is, the absence of an edge between $\evt{B}$ and $\evt{C}$ in the leftmost diagram asserts the independence of the output of $\evt{B}$ from the input of $\evt{C}$ and vice-versa. Hence, consistency with $\mathcal O$ implies consistency with any totalisation of $\mathcal O$.

For a process $\Phi$, a causal ordering $\mathcal O$, and a totalisation $\mathcal O'$ of $\mathcal O$, we have $\Phi \vDash \mathcal O \implies \Phi \vDash \mathcal O'$.

Assume $\Phi \vDash \mathcal O$. Then, for any subset $\mathcal E \subseteq \mathcal O$, there exists a process $\Phi'$ such that:

\begin{equation}\label{eq:sat-O}
\tikzfig{satisfies-O}
\end{equation}

But since $e \preceq_{\mathcal O} e' \implies e \preceq_{\mathcal O'} e'$, we have $\past_{\mathcal O}(\mathcal E) \subseteq \past_{\mathcal O'}(\mathcal E)$. Hence (<ref>) implies that $\Phi$ factors as required by Definition <ref>:

\begin{equation*}
\tikzfig{satisfies-Op}
\end{equation*}

Therefore $\Phi \vDash \mathcal O'$.

Combining this with its converse yields the following theorem.

For a process $\Phi$ and a causal ordering $\mathcal O$, $\Phi \vDash \mathcal O$ if and only if, for every totalisation $\mathcal O'$ of $\mathcal O$, $\Phi \vDash \mathcal O'$.

$(\Rightarrow)$ follows immediately from Lemma <ref>.
For $(\Leftarrow)$, let $\mathcal E \subseteq \mathcal O$ be any subset.
Split $\mathcal O$ into two parts, $\mathcal O_1 := \past_{\mathcal O}(\mathcal E)$
and $\mathcal O_2 := \mathcal O \backslash \past_{\mathcal O}(\mathcal E)$.
Define a total ordering $\mathcal O'$ on $\mathcal O_1 \cup \mathcal O_2$
by requiring that every element in $\mathcal O_1$ is below every element in $\mathcal O_2$
and taking any totalization on $\mathcal O_1$ and $\mathcal O_2$.
This order refines $\mathcal O$ because $\past_{\mathcal O}(\mathcal E)$ is downward-closed,
and by construction $\past_{\mathcal O}(\mathcal E) = \past_{\mathcal O'}(\mathcal E)$.
Hence $\Phi \vDash \mathcal O'$ implies:

Since we can find a suitable totalisation to give the equation above for any subset $\mathcal E \subseteq \mathcal O$, we have $\Phi \vDash \mathcal O$.

Hence, we can always replace consistency with a causal ordering with consistency with all of its totalisations, i.e., all of the linear orders which refine it. For example:

\begin{equation}\label{eq:totalise-order}
\tikzfig{big-phi-3} \ \vDash\ \tikzfig{common-cause}
\qquad \iff \qquad
\left(\ \
\tikzfig{big-phi-3} \ \vDash\ \tikzfig{common-cause-lin1}
\quad \wedge \quad
\tikzfig{big-phi-3} \ \vDash\ \tikzfig{common-cause-lin2}
\ \ \right)
\end{equation}

We already showed in the previous section that we can capture any linear ordering via combs. Hence, to capture any causal ordering, we only need to be able to take conjunctions of linear causal orders. This can be accomplished via intersections of types, much like those defined in [33] for the quantum case.

The types on the RHS of (<ref>) are, respectively:

\[
\bm X := \bm A \limp (\bm A' \limp (\bm B \limp \bm B') \limp \bm C) \limp \bm C'
\qquad\textrm{and}\qquad
\bm X' := \bm A \limp (\bm A' \limp (\bm C \limp \bm C') \limp \bm B) \limp \bm B'
\]

Our goal now is to form the intersection $\bm X \cap \bm X'$, which will consist precisely of those causal processes consistent with the causal ordering given by $\bm X$ and the one given by $\bm X'$. Categorically, intersections are given by pullback, so our first goal will be to find an object in which both $\bm X$ and $\bm X'$ embed. Since combs are special cases of causal processes, we can embed both $\bm X$ and $\bm X'$ into the system of all causal processes of the appropriate type, namely:

\[ \bm X \hookrightarrow (\bm A \otimes \bm B \otimes \bm C \limp \bm A' \otimes \bm B' \otimes \bm C') \hookleftarrow \bm X' \]

In fact, we can always find such embeddings for any system built inductively from first-order systems:

Any object $\bm X$ built inductively from first order systems $\bm A_1, \ldots, \bm A_m, \bm A_1', \ldots, \bm A_n'$ has a canonical embedding of the form:

\[ e : \bm X \rightarrow (\bm A_1 \otimes \ldots \otimes \bm A_m \limp \bm A_1' \otimes \ldots \otimes \bm A_n') \]

whose underlying $\mathcal C$-morphism is just a permutation of systems.

The proof is a straightforward application of the embedding $\bm A \otimes \bm B \hookrightarrow \bm A \parr \bm B$ and the special property of first order systems that $\bm A \otimes \bm B \cong \bm A \parr \bm B$. It is given explicitly in the appendix.

We will construct $\bm X \cap \bm X'$ essentially in terms of a set-theoretic intersection of their associated states $c_{\bm X}$ and $c_{\bm X'}$. For that, we we make use of the following lemma.

Let $c$ and $d$ be sets of states for the same object $A$ which are flat, closed, and furthermore satisfy the property that $\lambda \mmix \in c$ and $\lambda \mmix \in d$ for a fixed scalar $\lambda$. Then $c \cap d$ is also flat and closed.

For both properties, we rely on the fact that $(-)^*$ is order-reversing. That is, $a \subseteq b \Rightarrow b^* \subseteq a^*$. For flatness, we have by assumption that $\lambda \mmix \in c \cap d$. Since $c \cap d \subseteq c$, we have $c^* \subseteq (c \cap d)^*$. So by flatness of $c$, $\mu \disc \in c^*$ for some $\mu$. Hence $\mu \disc \in (c \cap d)^*$ and $c \cap d$ is flat.

For closure, first note that any set of states is contained in its double dual, so we have $c \cap d \subseteq (c \cap d)^{**}$.
For the converse, $c \cap d \subseteq c$ implies $c^* \subseteq (c \cap d)^*$ and similarly $d^* \subseteq (c \cap d)^*$. Hence, $c^* \cup d^* \subseteq (c \cap d)^*$, so $(c \cap d)^{**} \subseteq (c^* \cup d^*)^*$. It therefore suffices to show that $(c^* \cup d^*)^* \subseteq c \cap d$. This follows from the fact that $c^* \subseteq c^* \cup d^*$, so $(c^* \cup d^*)^* \subseteq c^{**} = c$ and similarly $(c^* \cup d^*)^* \subseteq d^{**} = d$.

Let $\bm X, \bm X'$ be a pair of objects with canonical embeddings $e, f$ into a fixed system $\bm Y := \bm A_1 \otimes \ldots \otimes \bm A_m \limp \bm A_1' \otimes \ldots \otimes \bm A_n'$,
as in Theorem <ref>. Then there exists an object $\bm X \cap \bm X'$ and morphisms $p_1, p_2$ in $\Caus[\mathcal C]$ making the following pullback:

\begin{equation}\label{eq:pullback}
\xymatrix{
\bm X \cap \bm X' \ar[d]^{p_2} \ar[r]^{p_1} & \bm X \ar[d]^{e} \\
\bm X' \ar[r]^{f}  & \bm Y
\end{equation}

Let $\bm Y := (Y, c_{\bm Y})$ and define the following two sets of states for $\bm Y$:

\begin{align*}
\overline{c}_{\bm X} & := \{ e \circ \rho \, | \, \rho \in c_{\bm X} \} \\
\overline{c}_{\bm X'} & := \{ f \circ \rho \, | \, \rho \in c_{\bm X'} \}
\end{align*}

Since $e$ and $f$ are just permutations of systems, it is straightforward to show that both of these sets are flat, closed, and  both contain $\lambda \mmix$ for some fixed $\lambda$. Hence, applying Lemma <ref>, we have that $\overline{c}_{\bm X} \cap \overline{c}_{\bm X'}$ is flat and closed. Then, let $\bm X \cap \bm X' := (Y, \overline{c}_{\bm X} \cap \overline{c}_{\bm X'})$, $p_1 := e^{-1}$ and $p_2 := f^{-1}$. It is straightforward to check that $p_1, p_2$ are indeed $\Caus[\mathcal C]$-morphisms and diagram (<ref>) clearly commutes.

It only remains to show that, for any $g: \bm Z \to \bm X$ and $h: \bm Z \to \bm X'$ such that $e \circ g = f \circ h$, there is a unique mediating morphism $z : \bm Z \to \bm X \cap \bm X'$:

\begin{equation*}
\xymatrix{
\bm Z \ar[rrd]^{g} \ar[rdd]_{h} \ar@{.>}[rd]|-{\,z\,} & & \\
& \bm X \cap \bm X' \ar[d]^{f^{-1}} \ar[r]_{e^{-1}} & \bm X \ar[d]^{e} \\
& \bm X' \ar[r]^{f}  & \bm Y
\end{equation*}

Since $e$ and $f$ are isomorphisms, the only possibility is $z := e \circ g = f \circ h$. So, it suffices to show that $z$ is a morphism in $\Caus[\mathcal C]$. For any $\rho \in c_{\bm Z}$, $g \circ \rho \in c_{\bm X}$, so $z \circ \rho = e \circ g \circ \rho \in \overline{c}_{\bm X}$. Similarly, $z \circ \rho = f \circ h \circ \rho \in \overline{c}_{\bm X'}$. Hence $z \circ \rho \in \overline{c}_{\bm X} \cap \overline{c}_{\bm X'}$, which completes the proof.

Since combs embed into all causal processes, it immediately follows that we can take intersections of combs via pullback. Hence, the condition on $\Phi$ stated in (<ref>) can equivalently be given in terms of $\Phi$ having the following type:

\[
\tikzfig{big-phi-3} : (\bm A \limp (\bm A' \limp (\bm B \limp \bm B') \limp \bm C) \limp \bm C') \cap (\bm A \limp (\bm A' \limp (\bm C \limp \bm C') \limp \bm B) \limp \bm B')
\]

This generalises in the obvious way to any causal ordering $\mathcal O$.

The fact that $\cap$ arises as a pullback also gives us some properties of intersections `for free'. For instance, any functor with a left adjoint necessarily preserves limits. By the definition of $*$-autonomous categories, $(\bm B \limp -)$ has a left adjoint given by $(- \otimes \bm B)$, so the following is immediate:

For objects $\bm A, \bm A'$ and $\bm B$ in we have

\[
\bm B \multimap (\bm A \cap \bm A') \cong (\bm B \limp \bm A) \cap (\bm B \limp \bm A')
\]

§ HIGHER-ORDER SYSTEMS WITH INDEFINITE CAUSAL ORDER

In this section we shall take a look at process matrices, introduced in [31],
to investigate processes which do not have a definite causal order.
Such processes were called bipartite second-order causal in [26].

A process $w : (A^{*} \otimes A') \otimes (B^{*} \otimes B') \to C^{*} \otimes C$
is called bipartite second-order causal ($\textrm{SOC}_2$)
if for all causal $\Phi_{A}, \Phi_{B}$ the following map is causal:

So $\textrm{SOC}_2$ maps send products of causal processes to a causal process.
The following shows that $\textrm{SOC}_2$ processes are actually normalized on all
non-signalling maps, not just product maps.

For first order systems $\bm A, \bm A', \bm B, \bm B', \bm C, \bm C'$,
a process $w$ is $\textrm{SOC}_2$ if and only if it is of type
$(\bm A \multimap \bm A') \otimes (\bm B \multimap \bm B') \multimap (\bm C \multimap \bm C')$.

Since products of causal processes are non-signalling, they are in $(\bm A \multimap \bm A') \otimes (\bm B \multimap \bm B')$, so any process of the above type is indeed $\textrm{SOC}_2$.

For the converse, let $\pi$ be an effect of type $(\bm C \multimap \bm C')^*$.
Then $\pi \circ w$ is an effect on products of causal processes.
Now Lemma <ref> states that $\pi \circ w$ yields $1$ for product states if and only if it yields $1$ for any state in the tensor product. Hence it is an effect for $(\bm A \multimap \bm A') \otimes (\bm B \multimap \bm B')$,
which by Theorem <ref> are precisely the non-signalling maps.
By Proposition <ref> this means $w: (\bm A \multimap \bm A') \otimes (\bm B \multimap \bm B') \multimap (\bm C \multimap \bm C')$

This represents a significant strengthening of the result in [26], which was only able to show that $\textrm{SOC}_2$ extends to all so-called strongly non-signalling processes, which are a special case of non-signalling processes.

Special cases of $\textrm{SOC}_2$ processes are 3-combs which arise from fixing a causal ordering between $\bm A$ and $\bm B$:

\begin{eqnarray*}
\bm C \limp (\bm A \limp (\bm A' \limp \bm B) \limp \bm B') \limp \bm C'\\
\bm C \limp (\bm B \limp (\bm B' \limp \bm A) \limp \bm A') \limp \bm C'\vspace{-0pt}
\end{eqnarray*}

Indeed one can show the containment of either of these types into the type of $\textrm{SOC}_2$ processes using a simple calculation on types much like in Remark <ref>. However, the most interesting $\textrm{SOC}_2$ processes are those which do not arise from combs.

The OCB process is defined as follows:

where $\sigma_x, \sigma_z$ are Pauli matrices and associated effects. Note that, while the individual summands are not positive, the result is, yielding a process in . The fact that it is an $\textrm{SOC}_2$ process in $\Caus[\CPM]$ follows straightforwardly from the fact that the Pauli matrices are trace-free. Furthermore, it was shown in [31] that it can be used to win certain non-local games with higher probability than any causally-ordered process, due to the fact that Bob can, to some extent, choose a causal ordering between himself and Alice a posteriori by his choice of quantum measurement.

Theorem <ref> extends naturally to a characterisation of $n$-partite second-order causal processes ($\textrm{SOC}_n$) via:

\[ (\bm A_1 \limp \bm A_1') \otimes \ldots \otimes (\bm A_n \limp \bm A_n') \limp (\bm C \limp \bm C') \vspace{-0pt}\]

Not all processes exhibiting indefinite causal order are quantum. Indeed the following process:
is an $\textrm{SOC}_3$ process in $\Caus[\MatRp]$, where the `$-$' labelled states and effects
are column vectors and row vectors with values $(1,-1)$ , respectively.

It was shown in [3] that this process, as well as a generalisation to an $\textrm{SOC}_n$ process for odd $n$, was incompatible with any pre-defined causal order.

An interesting family of $\textrm{SOC}_2$ processes are switches, where an auxiliary system is used to control the causal ordering of the input processes.

For first-order systems $\bm X$ and $\bm A = \bm A' = \bm B = \bm B' = \bm C = \bm C'$, a switch is a process of type:

\begin{equation}\label{eq:switch}
\tikzfig{switch}\ \ : \bm X \otimes \bm C \limp (\bm A \limp \bm A') \otimes (\bm B \limp \bm B') \limp \bm C'\vspace{-0pt}
\end{equation}

in , such that for distinct states $\rho_0, \rho_1 : \bm X$, we have:

\begin{equation}\label{eq:switch-eqs}
\tikzfig{switch0} \qquad \tikzfig{switch1}\vspace{-0pt}
\end{equation}

We now see some concrete examples of the switch, as a higher-order stochastic map and as a quantum channel.

For $\mathcal C = \MatRp$, the classical switch process is uniquely fixed by (<ref>) if we let $\bm X = 2$ and:

\[
\rho_0 := \left(\begin{matrix}
1 \\ 0
\end{matrix}\right)
\qquad
\rho_1 := \left(\begin{matrix}
0 \\ 1
\end{matrix}\right) \vspace{-0pt}\]

Indeed, $s$ is given by:

\begin{equation}\label{eq:switch-class}
\tikzfig{switch-class}\vspace{-0pt}
\end{equation}

where $\rho_i' := \rho_i^T$. Then, since $\rho_0' + \rho_1' = \disc$, we have:

Hence $s$ has the correct type shown in (<ref>).

For $\mathcal C = \CPM$, a switch process can be defined just as in (<ref>), by letting $\bm X = \mathcal L(\mathbb C^2)$ and replacing $\rho_i$ and $\rho_i^T$ with the appropriate qubit projections and their associated quantum effects:

\[ \rho_i := \ketbra{i}{i} \qquad\qquad \rho_i'(\mu) := \textrm{Tr}(\ketbra{i}{i}\mu) \vspace{-0pt}\]

This is precisely the $\mathcal Z$ superoperator defined in [8], which defines a (decoherent) switch for quantum channels.

However, unlike Example <ref>, this channel is not uniquely fixed by (<ref>), since $\rho_0, \rho_1$ do not form a basis for $\mathcal L(\mathbb C^2)$.
For instance, plugging $\rho := \ketbra{+}{+}$ into $\bm X$ of this process yields a classical mixture of the two possible wirings:
One can also define a coherent quantum switch which does satisfy (<ref>), but where inputting the state $\ketbra{+}{+}$ into $\bm X$ yields a quantum superposition of causal orderings. See [8] for details.

A switch cannot be causally ordered. That is, the type of $s$ does not restrict to one of the following:

\begin{eqnarray*}
\bm X \otimes \bm C \limp (\bm A \limp (\bm A' \limp \bm B) \limp \bm B') \limp \bm C'\\
\bm X \otimes \bm C \limp (\bm B \limp (\bm B' \limp \bm A) \limp \bm A') \limp \bm C'\vspace{-0pt}
\end{eqnarray*}

unless $\bm A \cong \bm I$.

Suppose $s$ is causally ordered with $\evt A \preceq \evt B$. That is:

\[ s : \bm X \otimes \bm C \limp (\bm A \limp (\bm A' \limp \bm B) \limp \bm B') \limp \bm C'\vspace{-0pt} \]

Plugging states and effects into $s$ yields a simpler type:

\begin{equation}\label{eq:switch-plug}
\tikzfig{switch-plug}\ \ :\ (\bm A \limp (\bm A' \limp \bm B) \limp \bm B')^*
\end{equation}

By Theorem <ref> characterising one-way signalling processes, one can verify that for any $\Phi : \bm A \limp \bm B'$, we have:

\[ \tikzfig{signal-single}\ \ :\ \bm A \limp (\bm A' \limp \bm B) \limp \bm B' \vspace{-0pt}\]

Since this is the dual type of (<ref>), composing the two yields

\[ \tikzfig{switch-plug1}\ =\ \tikzfig{time-travel2} \vspace{-0pt}\]

which violates no time-travel, Theorem <ref>. Hence $\bm A \cong \bm I$. The second causal ordering can be ruled out symmetrically, by plugging the state $\rho_0$ into $s$.

§ CONCLUSION AND FUTURE WORK

In order to study higher order processes, we have created a categorical construction
which sends certain compact closed categories $\mathcal C$ to a new category $\CausC$.
There is a fully faithful embedding of the category of first order causal processes of $\mathcal C$ into $\CausC$,
but we are also able to talk about genuine higher order causal processes.
This new category also has a richer structure which allows us to develop a type theory for its objects.
We classify certain kinds of processes in this type theory,
such as the non-signalling processes, one-way signalling processes, combs and bipartite second order causal processes and show that the type theoretic characterisation of these processes coincides with the operational one involving discarding.

The construction of can be generalised straightforwardly to encompass `sub-causal' processes as well, by replacing the definition of $(-)^*$ with:

\[ c^* = \{\pi:A^* \mid \forall x\in c, \pi \circ x \in \mathcal{M}\} \vspace{-0pt}\]

for a suitable sub-monoid $\mathcal M$ of $\mathcal C(I,I)$ to get $\Caus_{\mathcal M}[\mathcal C]$.
Then, we recover as $\Caus_{\{1\}}[\mathcal C]$. However, we obtain other interesting examples by varying $\mathcal M$. In the case of $\MatRp$, $\mathcal I = \mathbb R_+$. Taking $\mathcal M$ to be the unit interval, $\Caus_{[0,1]}[\mathcal C]$ gives us the full subcategory of probabilistic coherence spaces on finite sets [17]. Similarly, $\Caus_{[0,1]}[\mathcal C]$ has trace non-increasing CP maps as its first-order processes, and generalisations thereof at higher orders. Alternatively, we can build a category of `causal processes with failure' by letting $\mathcal M$ be $\{0,1\}$. Exploring the properties of these categories, and how they relate to is a subject of future work.
Another subject for future research is the relation between the types of causal systems and multiplicative linear logic (MLL).
Since $*$-autonomous categories are a model of MLL, MLL provides a (decidable) fragment of the logic of type containment in . This opens up possibilities to automate many proofs using existing automated linear logic provers. Indeed many of the type relationships in this paper were discovered with the help of such a tool, called  [39] (see Fig. <ref>).

Proving a 3-comb with trivial input and output systems embeds in $\SOCt$ using .

A third direction for future work is to understand exactly how expressive the internal logic of a HOCC is.
We showed in this paper that it is possible to express generalised conditional independences of a `non-signalling' variety,
which always takes a certain form for a process with inputs and outputs (e.g., a conditional probability distribution):

\[ \textrm{(outputs)} \indep \textrm{(inputs)} \ |\ \textrm{(other inputs)} \]

For example, the usual 2-party non-signalling conditions for a process $\Phi : A \otimes B \to A' \otimes B'$ are of the form:

\[
A' \indep B \ |\ A
\qquad\textrm{and}\qquad
B' \indep A \ |\ B
\]

However, classical conditional indepedences can be of the form $\mathcal A \indep \mathcal B \ |\  \mathcal C$ for arbitrary sets of random variables $\mathcal A, \mathcal B, \mathcal C$. It is therefore natural to ask if we could express such indepedences within a HOCC, possibly with some extra structure. One possible approach is to inter-convert inputs and outputs via the probabilistic operation of disintegration. This classical technique of converting a joint state into a reduced state and a conditional distribution is a crucial `subroutine' in Bayesian inference, and has recently given a categorical/string-diagrammatic characterisation by Cho and Jacobs [9] and showed that categories that admit disintegration enable various equivalent expressions of (arbitrary) conditional independences of systems, and can even recover the graphoid axioms of Verma and Pearl [40]. Thus, considering precausal categories with disintegration should enable one to say much more about conditional independences (and processes which preserve them) than just plain precausal categories. Unfortunately, disintegration in its usual form relies crucially on the copiability of classical data, so it does not have a straightforward quantum analogue. Nonetheless, quantum analogues to Bayesian conditioning [29] and more recently quantum common causes [2] could provide a solution analogous to the classical case.

Pushing this a bit further, one not only wishes to talk about independences within a HOCC, but also draw causal conclusions. That is, one not only wishes to rule out possible causal explanations, but also one wants to say when a causal influence is present (and possibly even measure it). Exploring the connection with techniques in classical causal inference of a logical or equational flavour, such as Pearl's do-calculus [32], may give some clues.

[1]
S. Abramsky and B. Coecke.
In Proceedings of the 19th Annual IEEE Symposium on Logic in
Computer Science (LICS), pages 415–425.

[2]
John-Mark A. Allen, Jonathan Barrett, Dominic C. Horsman, Ciarán M. Lee, and
Robert W. Spekkens.
Quantum common causes and quantum causal models.
Phys. Rev. X, 7:031021, Jul 2017.

[3]
Ä. Baumeler, A. Feix, and S. Wolf.
Maximal incompatibility of locally classical behavior and global
causal order in multiparty scenarios.
Phys. Rev. A, 90:042106, Oct 2014.

[4]
D. Beckman, D. Gottesman, M. A. Nielsen, and J. Preskill.
Causal and localizable quantum operations.
Phys Rev A, 64:052309, Nov 2001.

[5]
G. Chiribella, G. M. D'Ariano, and P. Perinotti.
Quantum circuit architecture.
Phys. Rev. Lett., 101:060401, Aug 2008.

[6]
G. Chiribella, G. M. D'Ariano, and P. Perinotti.
Theoretical framework for quantum networks.
Phys. Rev. A, 80:022339, Aug 2009.

[7]
G. Chiribella, G. M. D'Ariano, and P. Perinotti.
Informational derivation of quantum theory.
Physical Review A, 84(1):012311, 2011.

[8]
G. Chiribella, G. M. D'Ariano, P. Perinotti, and B. Valiron.
Quantum computations without definite causal structure.
Physical Review A, 88:022318, August 2013.

[9]
K. Cho and B. Jacobs.
Disintegration and Bayesian Inversion, Both Abstractly and
ArXiv e-prints, August 2017.

[10]
J.R.B. Cockett and R.A.G. Seely.
Proof theory for full intuitionistic linear logic, bilinear logic,
and mix categories.
Theory and Applications of Categories, 1991.

[11]
J.R.B. Cockett and R.A.G. Seely.
Weakly distributive categories.
Journal of Pure and Applied Algebra, 114(2):133 – 173, 1997.

[12]
B. Coecke.
Terminality equals non-signalling.

[13]
B. Coecke.
Terminality implies no-signalling ...and much more than that.
New Generation Computing, 34(1):69–85, 2016.

[14]
B. Coecke and A. Kissinger.
In Categories for the Working Philosopher.

[15]
Bob Coecke and Raymond Lal.
Causal categories: Relativistically interacting processes.
Foundations of Physics, 43(4):458, 2013.

[16]
Fabio Costa and Sally Shrapnel.
Quantum causal modelling.
New Journal of Physics, 18(6):063032, 2016.

[17]
Vincent Danos and Thomas Ehrhard.
Probabilistic coherence spaces as a model of higher-order
probabilistic computation.
Information and Computation, 209(6):966 – 991, 2011.

[18]
I. Ebert-Uphoff and Y. Deng.
Causal discovery for climate research using graphical models.
Journal of Climate, 25(17):5648–5665, 2012.

[19]
T. Eggeling, D. Schlingemann, and R. F. Werner.
Semicausal operations are semilocalizable.
EPL (Europhysics Letters), 57(6):782, 2002.

[20]
Karl Friston, Rosalyn Moran, and Anil K. Seth.
Analysing connectivity with granger causality and dynamic causal
Journal, Year.

[21]
Jean-Yves Girard.
Between logic and quantic: a tract.
Linear logic in computer science, 316:346–381, 2004.

[22]
G. Gutoski and J. Watrous.
Toward a general theory of quantum games.

[23]
J. Henson, R. Lal, and M. F. Pusey.
Theory-independent limits on correlations from generalized bayesian
New Journal of Physics, 16(11):113043, 2014.

[24]
M. Hyland and A. Schalk.
Glueing and orthogonality for models of linear logic.
Theoretical Computer Science, 294(1–2):183 – 231, 2003.

[25]
A. Kissinger, M. Hoban, and B. Coecke.
Equivalence of relativistic causal structure and process
ArXiv e-prints, 2017.

[26]
A. Kissinger and S. Uijlen.
Picturing indefinite causal structure.
In Quantum Physics and Logic, 2016.

[27]
Aleks Kissinger and Sander Uijlen.
A categorical semantics for causal structure.
In 32nd Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12,

[28]
M. Leifer.
The Choi-Jamiolkowski Isomorphism: You're Doing it Wrong!
Blog post,

[29]
M. S. Leifer and R. W. Spekkens.
Towards a formulation of quantum theory as a causally neutral theory
of bayesian inference.
Phys. Rev. A, 88:052130, Nov 2013.

[30]
S. Mac Lane.
Categories for the working mathematician.

[31]
O. Oreshkov, F. Costa, and C. Brukner.
Quantum correlations with no causal order.
Nature Communication, 1092(3).

[32]
J. Pearl.
Causality: Models, Reasoning and Inference.
Cambridge University Press, 2000.

[33]
P. Perinotti.
Causal structures and the classification of higher order quantum

[34]
Jacques Pienaar and Časlav Brukner.
A graph-separation theorem for quantum causal models.
New Journal of Physics, 17(7):073020, 2015.

[35]
N. Soranzo Pinna, A. and A. De La Fuente.
From knockouts to networks: establishing direct cause-effect
relationships through graph analysis.
PloS one, 5(10):e12912, 2010.

[36]
P. Selinger.
In New Structures for Physics.

[37]
Elena Sokolova, Perry Groot, Tom Claassen, Kimm J. van Hulzen, Jeffrey C.
Glennon, Barbara Franke, Tom Heskes, and Jan Buitelaar.
Statistical evidence suggests that inattention drives
hyperactivity/impulsivity in attention deficit-hyperactivity disorder.
PLoS one, 11(10):e0165120, 2016.

[38]
Peter Spirtes and Clark Glymour.
An algorithm for fast recovery of sparse causal graphs.
Social Science Computer Review, 9(1):62–72, 1991.

[39]
N. Tamura.
User's guide of a linear logic theorem prover (llprover).
Technical report, 1995.

[40]
Thomas VERMA and Judea PEARL.
Causal networks: Semantics and expressiveness.
In Ross D. SHACHTER, Tod S. LEVITT, Laveen N. KANAL, and John F.
LEMMER, editors, Uncertainty in Artificial Intelligence, volume 9 of
Machine Intelligence and Pattern Recognition, pages 69 – 76.
North-Holland, 1990.

[41]
Christopher J Wood and Robert W Spekkens.
The lesson of causal discovery algorithms for quantum correlations:
causal explanations of bell-inequality violations require fine-tuning.
New Journal of Physics, 17(3):033002, 2015.

§ OMITTED PROOFS

§.§ Proof that is $*$-autonomous

In this part of the appendix we will give full proofs leading up to the fact that is indeed a $*$-autonomous category.

$\CausC$ is an SMC, with tensor given by:

\[ \bm A \otimes \bm B := (A \otimes B, c_{\bm A \otimes \bm B}) \]

and tensor unit $\bm I := (I, \{1\})$.

First we show that $\bm A \otimes \bm B$ and $\bm I$ are indeed objects in , namely the $c_{\bm A \otimes \bm B}$ and $c_{\bm I}$ are flat and closed. This is immediate for $c_{\bm I}$, so we focus on $c_{\bm A \otimes \bm B}$.

Closure follows immediately from Lemma <ref>, so it remains to show flatness. Since $c_{\bm A}$ and $c_{\bm B}$ are flat, then for some $\lambda, \lambda'$:

\[ \lambda\ \maxmix \in c_{\bm A},\  \lambda'\ \maxmix \in c_{\bm B} \]

\[ \lambda\lambda'\ \maxmix\,\maxmix \in c_{\bm A} \otimes c_{\bm B} \subseteq c_{\bm A \otimes \bm B} \]

Similarly, for some $\mu, \mu'$:

\[ \mu\ \discard \in c_{\bm A}^*,\ \mu'\ \discard \in c_{\bm B}^* \]

So, for all $\rho \in c_{\bm A}$, $\rho' \in c_{\bm B}$, we have:

\[ \mu\mu'\ \weight{\rho}\, \weight{\rho'} = 1 \]

which implies, by Lemma <ref>:

\[ \mu\mu' \discard \, \discard \in (c_{\bm A} \otimes c_{\bm B})^* =
(c_{\bm A} \otimes c_{\bm B})^{***} =: c_{\bm A \otimes \bm B}^*\]

Next, we show associativity and unit laws for $\otimes$. For any object $\bm A$, the unit laws $\bm A \otimes \bm I = \bm A = \bm I \otimes \bm A$ follow from the closure of $c_{\bm A}$. Associativity is a bit trickier. We first work in terms of effects in order to take advantage of Lemma <ref>. Applying this to an effect $\pi \in c_{(\bm A \otimes \bm B) \otimes \bm C}^*$ gives:

\begin{align*}
\quant{\forall\ \Psi \in c_{(\bm A \otimes \bm B) \otimes \bm C}}{\tikzfig{tri-braket1}\ =\ 1}
& \ \ \iff\ \
\quant{\forall\ \Psi \in c_{\bm A \otimes \bm B}, \xi \in c_{\bm C}}{\tikzfig{tri-braket2}\ =\ 1} \\[3mm]
& \ \ \iff\ \
\quant{\forall\ \psi \in c_{\bm A}, \phi \in c_{\bm B}, \xi \in c_{\bm C}}{\tikzfig{tri-braket3}\ =\ 1}
\end{align*}

Similarly, for $\pi \in c_{\bm A \otimes (\bm B \otimes \bm C)}^*$

\begin{align*}
\quant{\forall\ \Psi \in c_{\bm A \otimes (\bm B \otimes \bm C)}}{\tikzfig{tri-braket1}\ =\ 1}
& \ \ \iff\ \
\quant{\forall\ \psi \in c_{\bm A}, \Phi \in c_{\bm B \otimes \bm C}}{\tikzfig{tri-braket2p}\ =\ 1}  \\[3mm]
& \ \ \iff\ \
\quant{\forall\ \psi \in c_{\bm A}, \phi \in c_{\bm B}, \xi \in c_{\bm C}}{\tikzfig{tri-braket3}\ =\ 1}
\end{align*}

Hence $c_{(\bm A \otimes \bm B) \otimes \bm C}^* = c_{\bm A \otimes (\bm B \otimes \bm C)}^*$ so $c_{(\bm A \otimes \bm B) \otimes \bm C} = c_{\bm A \otimes (\bm B \otimes \bm C)}$, which implies associativity of $\otimes$.

Next we show that $\otimes$ is well-defined on morphisms. For morphisms $f : \bm A \to \bm A'$, $g : \bm B \to \bm B'$, and an effect $\pi \in c_{\bm A' \otimes \bm B'}^*$, we have by Lemma <ref>:

\[
\quant{\forall\ \Psi \in c_{\bm A \otimes \bm B}}{\tikzfig{bi-braket-fg1}\ =\ 1}
\ \ \iff\ \
\quant{\forall\ \psi \in c_{\bm A}, \phi \in c_{\bm B}}{\tikzfig{bi-braket-fg2}\ =\ 1}
\]

The RHS holds since $f \circ \psi \in c_{\bm A'}$ and $g \circ \phi \in c_{\bm B'}$. From the LHS above, we can conclude that $f \otimes g : \bm A \otimes \bm B \to \bm A' \otimes \bm B'$ is a morphism in .

Finally, it remains to show that the swap is a morphism in . By Proposition <ref>, this is the case when, for all $\pi \in c_{\bm B \otimes \bm A}^*$, we have:

\[ \tikzfig{swap-effect}\ \in\ c_{\bm A \otimes \bm B}^* \]

This again follows by relying on Lemma <ref>.

The transposition functor $(-)^* : \mathcal C^{\textrm{op}} \to \mathcal C$:

\begin{equation}\label{eq:trans-functor}
A\mapsto A^* \qquad\qquad \tikzfig{transpose}
\end{equation}

lifts to a full and faithful functor $(-)^* : \CausC^{\textrm{op}} \to \CausC$, where $\bm A^* := (A^*, c_{\bm A^*})$.

Note that $c_{\bm B}^* = c_{\bm B^*}$, by definition, and $c_{\bm A} = c_{\bm A}^{**} = (c_{\bm A^*})^*$. Hence, for $f : \bm A \to \bm B$ we have:

\[ \quant{\ \forall\ \rho \in c_{\bm A}, \pi \in c_{\bm B}^*\ }{\tikzfig{dual-f1}\ =\ 1}
\ \ \iff\ \
\quant{\ \forall\ \pi \in c_{\bm B^*}, \rho \in (c_{\bm A^*})^*\ }{\tikzfig{dual-f2}\ =\ 1}  \]

so $f^* : \bm B^* \to \bm A^*$ is a morphism in .
Just as with the functor $(-)^*$ in $\mathcal C$, $((-)^*)^* = \textrm{Id}_{\CausC}$, so fullness and faithfulness is immediate.

For any precausal category $\mathcal C$, is a $*$-autonomous category where $\bm I = \bm I^*$.

We have already shown that is an SMC (Theorem <ref>) with a full and faithful functor
$(-)^* : \CausC^{\textrm{op}} \to \CausC$ (Lemma <ref>).
Consider objects $\bm A, \bm B, \bm C$ in . The underlying object of $\bm B \limp \bm C$ is:

\[ (B \otimes C^*)^* = B^{*} \otimes C^{**} = B^* \otimes C \]

Since $\mathcal C$ is compact closed, there is a natural isomorphism:

\[  \mathcal C(A \otimes B, C) \cong \mathcal C(A, B^* \otimes C) \]

given by:

\[ \tikzfig{fABtoC} \quad \mapsto \quad
\tikzfig{fAtoBstarC}\ \ =:\ \ \tikzfig{gAtoBstarC} \]

whose inverse is:

\[ \tikzfig{gAtoBstarC} \quad \mapsto \quad
\tikzfig{gABtoC} =\ \ \tikzfig{fABtoC} \]

Indeed this is how one shows that compact closed categories are in fact closed.
Thus, it suffices to show that:

\[ f \in \CausC(\bm A \otimes \bm B, \bm C) \iff g \in \CausC(\bm A, \bm B \limp \bm C) \]

This follows from Lemma (<ref>):

\begin{align*}
f \in \CausC(\bm A \otimes \bm B, \bm C)
&\ \iff \
\quant{\forall \rho \in c_{\bm A \otimes \bm B}, \pi \in c_{\bm C}^*}
{\tikzfig{fABtoC-sandwich1}\ =\ 1} \\[3mm]
& \iff \ \quant{\forall \rho_1 \in c_{\bm A}, \rho_2 \in c_{\bm B}, \pi \in c_{\bm C}^*}
{\tikzfig{fABtoC-sandwich2}\ =\ 1} \\[3mm]
&\ \iff \
\quant{\forall \rho_1 \in c_{\bm A}, \rho_2 \in c_{\bm B^*}^*, \pi \in c_{\bm C}^*}
{\tikzfig{fABtoC-sandwich3}\ =\ 1} \\[3mm]
&\  \iff \
g \in \CausC(\bm A, \bm B \limp \bm C)
\end{align*}

Finally, $\bm I = \bm I^*$ follows from the fact that $I = I^*$ and

\[c^*_{\bm I} = \{\lambda \mid 1 \lambda = 1\} = \{1\} = c_{\bm I} \]

§.§ Proofs that and are precausal

is a precausal category.

was given in Example <ref>. is immediate, and follows from the fact that one can always construct a basis for a vector space out of probability distributions, e.g., by taking the point distributions. To show , we will decompose into and via Proposition <ref>.

So, we turn to :

\[ \quant{\exists\ \Phi'\ \textit{causal}}{\tikzfig{one-way-sig}}
\implies
\quant{\exists\ \Phi_1,\Phi_2\ \textit{causal}}{\tikzfig{one-way-sig2}}
\]

In terms of a conditional probability distribution $P(B_1 B_2 | A_1 A_2)$, the premise above amounts to the usual non-signalling condition:

\[ P(B_1 | A_1 A_2) = P(B_1 | A_1) \]

Hence the conclusion follows from the product rule:

\begin{align*}
P(B_1 B_2|A_1 A_2) & = P(B_1 | A_1 A_2) P(B_2 | B_1 A_1 A_2) \\
&  = P(B_1 | A_1) P(B_2 | B_1 A_1 A_2)
\end{align*}

More precisely, suppose $\Phi_{ij}^{kl}$ is a stochastic matrix such that there exists another stochastic matrix $(\Phi')_i^k$ where:

\[ \sum_l \Phi_{ij}^{kl} = (\Phi')_i^k \]

Then, let:

\begin{align*}
(\Phi_1)_{i}^{ki'k'} & = (\Phi')_i^k \delta_{ii'} \delta_{kk'} \\
(\Phi_2)_{i'k'j}^l & = \begin{cases}
\delta_{0l} & \textrm{ if } (\Phi')_i^{k'} = 0 \\
\Phi_{ij}^{k'l}/(\Phi')_i^{k'} & \textrm{ otherwise}
\end{cases}
\end{align*}

where $\delta_{ij}$ is the Kronecker delta. One can straightforwardly verify that these are both stochastic matrices. Let $\Psi_{ij}^{kl}$ be the result of plugging outputs $i',k'$ of $\Phi_1$ into those inputs for $\Phi_2$, i.e.

\[
\Psi_{ij}^{kl}
:= \sum_{i'k'} (\Phi_1)_{i}^{ki'k'} (\Phi_2)_{i'k'j}^l
= (\Phi')_i^k (\Phi_2)_{ikj}^l
\]

If $(\Phi')_i^k = 0$, then both $\Phi_{ij}^{kl}$ and $\Psi_{ij}^{kl}$ are $0$ for all $j, l$. So, suppose $(\Phi')_i^k \neq 0$. Then:

\[ \Psi_{ij}^{kl}
= (\Phi')_i^k (\Phi_{ij}^{kl}/(\Phi')_i^k)
= \Phi_{ij}^{kl} \]

For , let $w_j^i$ be the matrix of a second-order causal effect $w : A \otimes B^*$. Then for all stochastic matrices $\Phi_i^j$, we have:

\[ \sum_{ij} w_j^i \Phi_i^j = 1 \]

For some fixed column $m$, and fixed rows $n \neq n'$, the following matrix:

\[
1 = \Phi_i^j = \begin{cases}
p & i = m, j = n \\
1 - p & i = m, j = n' \\
0 & i = m, j \neq n, j \neq n' \\
\delta_i^j & i \neq m
\end{cases}
\]

defines a stochastic map for any $p \in [0,1]$. Then:

\[ \sum_{ij} w_j^i \Phi_i^j = p w_n^m + (1-p) w_{n'}^m + K = 1 \]

where $K$ doesn't depend on $p$. Since we can freely vary $p$ between $0$ and $1$, the only way to preserve normalisation is if $w_n^m = w_{n'}^m$. Hence, for all $j$, we have $w_j^i = w_0^i$. Defining $\rho^i := w_0^i$ gives factorisation .

The category is a precausal category.

As noted in Example <ref>, discarding processes satisfying are given by the trace. For , $d_{\mathcal L(H)} = \textrm{dim}(H)^2$, which is invertible whenever $\textrm{dim}(H) \neq 0$. follows from the fact that for any finite-dimensional Hilbert space $H$, we can find a basis of positive operators spanning $\mathcal L(H)$. Hence, by renormalising, we can also find a basis of trace-$1$ positive operators.

For , we shall show and .

Condition states that

$$tr_{B'}(\Phi) = \Phi' \implies \Phi = (1_{A'} \otimes \Phi_2) \circ (\Phi_1 \otimes 1_B)$$

This is precisely the result of [19] and is based on the fact that minimal Stinespring dilations are related by a unitary.

For , a causal map $\Phi : A\to B$ in is a completely positive trace preserving map.
Such a map can always be written as
where the states and effects labeled with $i$ ($j$) form a basis for $B$ ($A^*$), with the 0-th basis element the maximally mixed state (discard effect).

Now if any second order causal effect $w$ does not split as in , we can always change the value of some of the $r_{i,j}$ such that $\Phi$ is still positive, but $w(\Phi) \neq 1$.

§.§ Proofs that is only weakly pre-causal

The category satisfies axioms -and .

It will be conventient to write relations as (possibly infinite) matrices taking entries the booleans. That is, a relation $f \subseteq A \times B$ is equivalently represented as the following boolean matrix:

\[ \left\{ f_i^j \in \mathbb B | i \in A, j \in B \right\} \]

Relation composition then becomes:

\[ h_i^k := \sum_j f_i^j g_j^k \]

where we interpret multiplication as meet and (possibly infinite) summation as join.

For , the discarding map for any system $A$ is the relation which relates every $i \in A$ to $* \in I := \{*\}$. That is:

\[ \discard_i = 1 \]

This clearly respects the monoidal structure. Using this definition of discarding, causal relations are those $f$ such that for all $i \in A$ there exists $j \in B$ such that $f_i^j = 1$.

The empty set is the zero object in . The definition of discarding yields that $d_A = 1$ for all non-empty sets $A$, hence is satisfied.

is immediate consequence of the fact that all singletons $\{i\} \subseteq A$ are causal states in .

can be proven in almost the same way as for . That only difference is we no longer need to use division in the definiton of $\Phi_2$, because $0$ and $1$ are the only possible values that $(\Phi')_i^{k'}$ can take:

\begin{align*}
(\Phi_1)_{i}^{ki'k'} & = (\Phi')_i^k \delta_{ii'} \delta_{kk'} \\
(\Phi_2)_{i'k'j}^l & = \begin{cases}
\delta_{0l} & \textrm{ if } (\Phi')_i^{k'} = 0 \\
\Phi_{ij}^{k'l} & \textrm{ if } (\Phi')_i^{k'} = 1
\end{cases}
\end{align*}

These are causal, and by case distinction on $(\Phi')_i^{k'} \in \{0, 1\}$, we can see that:

\[ \sum_{i'k'} (\Phi_1)_{i}^{ki'k'} (\Phi_2)_{i'k'j}^l = \Phi_{ij}^{kl} \]

The category does not satify .

Causality means for all $i$, there exists $j$ such that $f_i^j = 1$. The dual condition for causality is obtained by reversing the quantifies. That is, for some relation $w$:

\begin{equation}\label{eq:rel-soc}
f \ \ \textit{causal} \ \ \implies \ \ \sum_{ij} f_i^j w_j^i = 1
\end{equation}

if and only if there exists some $j$ such that for all $i$, $w_j^i = 1$.

requires that any such $w$ must be independent of $i$. That is, $w_j^i = \rho^i$. However, $w \subseteq \mathbb B \times \mathbb B$ defined by $w_j^i := \neg(i \wedge j)$ satisfies (<ref>), but is not independent of $i$.

§.§ Proof of embedding into the type of all causal processes

Any object $\bm X$ built inductively from first order systems $\bm A_1, \ldots, \bm A_m, \bm A_1', \ldots, \bm A_n'$ has a canonical embedding of the form:

\[ e : \bm X \rightarrow (\bm A_1 \otimes \ldots \otimes \bm A_m \limp \bm A_1' \otimes \ldots \otimes \bm A_n') \]

whose underlying $\mathcal C$-morphism is just a permutation of systems.

Given $\bm X$ built inductively from first-order types via the $*$-autonomous structure, we can replace $\bm A \limp \bm B$ with $\bm A^* \parr \bm B$ and push the $(-)^*$ inside as far as possible via application of the following isomorphisms from left-to-right:

\[
(\bm A \otimes \bm B)^* \cong \bm A^* \parr \bm B^*
\qquad \textrm \qquad
(\bm A \parr \bm B)^* \cong \bm A^* \otimes \bm B^*
\]

We can then apply $\bm A^{**} \cong \bm A$ to reduce $\bm X$ to an expression consisting of either first-order types or their duals, combined with $\otimes$ and $\parr$.
For example, if $\bm X := \bm A_1 \limp (\bm A_1' \limp \bm A_2) \limp \bm A_2'$, we have:

\begin{align*}
\bm X & := \bm A_1 \limp (\bm A_1' \limp \bm A_2) \limp \bm A_2' \\
& \cong \bm A_1^* \parr ((\bm A_1')^* \parr \bm A_2)^* \parr \bm A_2' \\
& \cong \bm A_1^* \parr ((\bm A_1')^{**} \otimes \bm A_2^*) \parr \bm A_2' \\
& \cong \bm A_1^* \parr (\bm A_1' \otimes \bm A_2^*) \parr \bm A_2'
\end{align*}

It was then noted in section <ref> that there is a canonical embedding $\bm A \otimes \bm B \hookrightarrow \bm A \parr \bm B$. We then apply this embedding to eliminate all $\otimes$'s, and then apply a permutation in $\mathcal C$ to sort all of the dual first-order systems to the left. Continuing the example, we have:

\begin{align*}
\bm X & \cong \bm A_1^* \parr (\bm A_1' \otimes \bm A_2^*) \parr \bm A_2' \\
& \hookrightarrow \bm A_1^* \parr \bm A_1' \parr \bm A_2^* \parr \bm A_2' \\
& \overset{(\dagger)}{\cong} \bm A_1^* \parr \bm A_2^* \parr \bm A_1' \parr \bm A_2'
\end{align*}

We can then pull the $(-)^*$ out as far as possible and re-introduce the $\limp$. Then, by Corollary <ref>, we can always replace a $\parr$ of first-order systems with a $\otimes$, which completes the embedding. Applying these steps to the running example yields:

\begin{align*}
\bm X & \cong \bm A_1^* \parr \bm A_2^* \parr \bm A_1' \parr \bm A_2' \\
& \cong (\bm A_1 \otimes \bm A_2)^* \parr \bm A_1' \parr \bm A_2' \\
& \cong \bm A_1 \otimes \bm A_2 \limp \bm A_1' \parr \bm A_2' \\
& \cong \bm A_1 \otimes \bm A_2 \limp \bm A_1' \otimes \bm A_2'
\end{align*}

We complete the proof by noting that the only step not arising from an identity morphism in $\mathcal C$ is the step marked $(\dagger)$ above, which is a permutation.