# A BV-Category of Spacetime Interventions

James Hefford, Matt Wilson

► To cite this version:

James Hefford, Matt Wilson. A BV-Category of Spacetime Interventions. 2025. hal-05213710

HAL Id: hal-05213710

https://hal.science/hal-05213710v1

Preprint submitted on 18 Aug 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A BV-Category of Spacetime Interventions

James Hefford*, Matt Wilson*†

* Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, CentraleSupélec, Laboratoire Méthodes Formelles

† University College London, PPLV Group

Email: james.hefford@inria.fr, matthew.wilson@centralesupelec.fr

***Abstract***—We use the Chu construction to functorially build BV-categories from duoidal categories, demonstrating that candidate models of BV-logic can be cofreely constructed from a fragment of a model of Retoré's sequencing operator. By using this construction to show that the strong Hyland envelope is a BV-category, we find a way to build a canonical model of spatio-temporal relationships between agents in spacetime from any symmetric monoidal category. The concrete physical interpretation of spacetime events in this model as intervention-context pairs resolves deficiencies in previous attempts to give a general categorical semantics to quantum supermaps.

## I. INTRODUCTION

From the perspective of abstract algebra, monoidal category theory provides a formalisation of circuit theories, that is, theories of processes with timelike and spacelike composition rules [1]. Along with the natural applications to quantum computer science, the existence of timelike and spacelike composition rules also forms the backbone of modern attempts to axiomatise quantum mechanics in terms of its compositional and operational features [2]–[4]. However, whilst monoidal structure captures a minimal notion of spacetime compatibility of a theory, it is not rich enough to provide a full account of the causal structure and correlations between spacetime events as conceptualised in the modern foundations of physics [5]–[7].

In this domain, spatio-temporal correlations are studied by modelling events in terms of the interventions that can be made by agents. Such agents possess the ability to perform experiments by choosing the settings and viewing the outcomes of devices in their local laboratories [6].

<figure><img src="image_2.png" /></figure>

This formulation of events in terms of the local interventions of agents motivates a dual picture of spacetime as a process-with-holes, referred to variously as the supermap [8]–[10], process matrix [6], or process tensor perspective [7]. These spacetime models are innately higher-order: a process-with-holes is interpreted as a context to be probed by the lower-order interventions of the local agents, thereby acting as a map on the processes of some monoidal category.

A number of important questions in the foundations of physics have prompted this conceptualisation of spacetime

events. For instance, contexts have been used to model quantum superpositions of causal structures which, if realisable, would allow for computations and correlations beyond those that can be produced in a classical spacetime [5], [11]. They have further been used to cleanly define quantum non-Markovian dynamics [7], and generalise causal modelling to the quantum setting [12]. Along with ongoing interest in the properties of correlations that can be extracted from processes-with-holes [6], there has been recent interest in both generalising these models to the study of alternative physical theories [13]–[18] and finding more abstract logical and categorical models which can adequately cope with higher-order causal structures [18]–[28].

With the understanding that a fully-fledged model of spatio-temporal correlations requires us to move from processes to spacetime events, we expect that we should move away from mere monoidal categories to a more capable logical system. The deep inference system BV is one such logic originating in the study of extensions of multiplicative linear logic (MLL) to incorporate non-commutativity [29]–[32]. BV-logic is defined in terms of the *calculus of structures* and adds a non-commutative sequencing operator $\otimes$ to the multiplicative conjunction $\otimes$ and disjunction $\nvdash$ of MLL [31]. These structures permit the following graphical depiction.

<figure><img src="image_3.png" /></figure>

The similarity between these structures and spacetime diagrams is particularly notable. Indeed, the analogy between the operators $\otimes$, $\otimes$ and $\nvdash$ and spatio-temporal correlations was appreciated in the seminal [31]. Upon interpreting the $P_i$ as the agents, we see that $\otimes$ forbids communication, $\nvdash$ allows arbitrary communication and $\otimes$ permits just one directional communication. Indeed, Guglielmi suggests a broad interpretation of $\otimes$ as temporal composition with $P_2 \otimes P_1$ thought of as “$P_1$ before $P_2$”.

## A. Related Work

BV-logic has been related to causality in quantum physics in at least two ways before: by connection to the causal set approach to quantum gravity [33], [34], and by connection to
the study of higher-order quantum theory and indefinite causal orders [19], [20]. The former [33] introduced the study of discrete quantum causal dynamics (DQCD) to track the causal evolution of density matrices through foliations of a classical spacetime. Spacetime events are considered to be vertices of a directed acyclic graph (DAG) with the edges representing causal links between the events. Quantum systems are then placed over these DAGs with their evolutions compatible with the causal structure. It was later demonstrated that the structure of these quantum causal evolutions could be interpreted as models of the system BV with the intuitive interpretation of the connectives given in equation (2) [34]. Two concrete examples of categories which gave semantics to this logical syntax were given: the probabilistic and quantum coherence spaces of [35]. DQCD is, however, restricted to first order: it tracks the evolution of states through spacetime but does not carry a notion of event as an intervention or a hole, and likewise does not carry a notion of higher-order process.

The other notable connection between BV-logic, causal-
ity and quantum theory was developed in [19], [20]. This
introduced the Caus-construction (as an instance of double
gluing) and demonstrated that the higher-order processes of
finite dimensional classical and quantum theory form BV-
categories. Within these categories are not only the expected
first-order evolutions of systems but also the higher-order
maps arising in the supermap framework. What is surprising
however is the specificity of the construction, with the Caus-
construction only working in particular instances and not
permitting the study of spatio-temporal correlations between
systems from arbitrary physical theories. This includes infinite
dimensional quantum theory, in addition to a myriad of other
exotic models stemming from Operational and Categorical
Probabilistic Theories [2], [3].

Another approach to modelling quantum supermaps was
presented in [22] developing on [15], [21]. A general definition
for higher-order transformations over any symmetric monoidal
category was first presented in [15] and demonstrated to
recover the usual definition in the case of finite dimensional
quantum theory. This definition was reinterpreted in [22] to
show that the required algebraic laws are precisely those of
a strong natural transformation between strong profunctors.
With this identification in place and by noting that strong
endoprofunctors form a duoidal category [36]–[38], it was
possible to endow the earlier models of [15], [21] with tensor
products ⊗ and ⊖ which faithfully model the causally ordered
and non-ordered supermaps. Lacking from this model was
any richer logic: it was noted that the natural candidates
for a negation or ℘ failed to be involutive and associative
respectively, and thus failed to give a model of MLL or indeed
BV.

The search for models of BV-logic leads us naturally to the
study of its categorical semantics, which appears to have not
been particularly deeply studied in the literature. Although a
notion of BV-category was suggested in [39], even the basic
notions of BV-functors and BV-natural transformations are
absent from the literature, and these are vital not only in

the development of the theory of BV-categories themselves,
but also in comparisons between physical models of spatio-
temporal correlations exhibiting this logic. We also note that,
as far as we are aware there is yet to be a definitive notion of
a model of BV-logic. While this is not a topic we are going to
address here, the BV-categories of [39] can be placed on a firm
algebraic footing and appear to fulfil at least the minimal of
demands to interpret the system BV. Sadly, no general methods
for constructing BV-categories have appeared in the literature,
and the only widely known non-trivial examples (where ⊗,
⊗ and ℘ all differ) are those we have earlier discussed. The
closest we have found to a result in this direction appears in
[40] where it is proven that the Chu construction [41], [42]
sends duoidal pomonoids to BV-pomonoids. To categorify this
result would require the upgrading of pomonoids to monoidal
categories while dealing with all the additional coherence data.

This leaves us with two thoughts: 1) that there should exist
some deeper connection between monoidal categories and
models of BV-logic, and 2) that such a connection would not
only be a rich source of models of the system BV, but that this
source could be used to develop the study of spatio-temporal
correlations in less well understood domains such as infinite
dimensional quantum theory or in generalised probabilistic
theories. Encouraged by the relevance of these thoughts to
both physics and logic, we aim to study the question of how
to construct from any monoidal category, its associated BV-
category of events.

B. Contributions

We prove that the Chu construction sends closed normal du-
oidal categories to BV-categories, categorifying a result of [40]
showing that the Chu construction sends duoidal pomonoids
to BV ones. Along the way, we reframe the definition of BV-
categories to show that they are pseudomonoids in a 2-category
of *-autonomous categories placing them on a firmer algebraic
footing. This allows us to define the 2-category BV of BV-
categories, BV-functors and BV-transformations and handle
all the coherence data in a concise manner. We are then able
to prove that the Chu construction is a right 2-adjoint to the
forgetful functor $U$ from BV-categories to normal $\otimes$-closed,
$\otimes$-symmetric duoidal categories, lifting the well-known 2-
adjunction between closed symmetric monoidal categories and
*-autonomous ones [43].

$$
\mathrm{CSNDuo} \xrightarrow[\substack{\leftarrow \\ U}]{\mathrm{Chu}} \mathrm{BV}
$$

This allows us to construct cofree BV-categories over the
fragment given by multiplicative conjunction ⊗, sequencing
⊗ and a weak dualising operator (-)* = [-, ⊥]. While it is
already very well-known that Chu(*C*, ⊥) is a model of linear
logic, the interesting part here is that the tensor product ⊗ can
be lifted to give a sequencing operator on Chu(*C*, ⊥) with the
required self-duality and distributive structures with respect to
the tensor ⊗ and par ℘.

With this tool at hand, we build upon the work of [22]
by studying a modified version of the Hyland envelope [44],
[45] which we dub the strong Hyland envelope. Explicitly, this category StEnv($C$) := Chu(StProf($C$), 1) is given by taking the Chu construction of strong endoprofunctors with the identity profunctor 1 := $C(-, -)$ as the dualising object. Since StProf($C$) is normal duoidal, StEnv($C$) is a BV-category by our general result. This completes a series of canonical free and cofree constructions starting from any symmetric monoidal category $C$.

$$C \stackrel{D}{\rightsquigarrow} C \times C^{\text{op}} \rightsquigarrow \text{Prof}(C) \stackrel{N}{\rightsquigarrow} \text{StProf}(C) \stackrel{\text{Chu}}{\rightsquigarrow} \text{StEnv}(C)$$

Here, $D$ is the doubling (splicing) construction of [37]; $y$ is the free cocompletion; $N$ is the normalisation of duoidal categories [36], [37]; and Chu is the Chu construction [41], [42]. Besides $\otimes$ which is lifted all the way along this series of adjunctions, all the other logical connectives ($\otimes$, $\mathcal{N}$ and $(-)^*$) alongside their necessary interaction, are (co)freely added.

We then justify our claim that StEnv($C$) is not just a canonical BV-category, but a physically relevant one that develops and brings together aspects of those already in the literature.

The objects of StEnv($C$) consist of intervention-context pairs. This unites the two dual views of spacetime events: an event is no longer just the local actions of an agent, nor the hole in a process, but a unification of the two. The causal relationships between these events are captured by the tensors $\otimes$, $\otimes$ and $\mathcal{N}$ which act on the interventions in the following fashion.

<figure><img src="image_4.png" /></figure>

These tensors come equipped with distributors which act as,

<figure><img src="image_5.png" /></figure>

<figure><img src="image_6.png" /></figure>

This improves on the weak logical structure of the model of [22] in a physically meaningful way: the new connective $\mathcal{N}$ models the possibility of arbitrary causal communication between agents and $(-)^*$ models the duality between interventions and contexts. We also gain the expected distributive laws between the new $\mathcal{N}$ connective and the existing $\otimes$ and $\otimes$.

StEnv($C$) unites ideas behind both the Caus-construction and discrete quantum causal dynamics. On the one hand, our model is manifestly higher-order like the Caus-construction, while being able to provide a BV-category of spacetime events over any symmetric monoidal category. Thus it can handle situations that are untreatable by the Caus-construction. On the other hand, the similarity between the DAGs of discrete quantum causal dynamics and profunctors should be appreciated. One can understand, at least at an intuitive level, why our model is BV by seeing the profunctors as ways of “inflating” the DAGs and inhabiting them with processes.

<figure><img src="image_7.png" /></figure>

At the same time, the higher-order transformations that are present in StEnv($C$) appear to be lacking from discrete quantum causal dynamics.

The interventions and contexts that can be studied within StEnv($C$) can take many exotic forms. This includes objects like that depicted in equation (3); bipartite interventions modelling an agent probing an experimental device; comb-like contexts; and arbitrary black-box supermaps like the quantum switch. One benefit of this flexibility is that one can demand decompositional properties of higher-order transformations by studying certain intervention-context pairs. For instance, we can ensure that all single-party supermaps possess a factorisation as a comb without requiring any properties of our starting symmetric monoidal category. This has wider effects, like demanding that multi-partite higher-order transformations possess local comb decompositions. This idea was considered in [21] as a way of defining a $\mathcal{N}$ in StProf($C$) and here we see the strong Hyland envelope providing a cleaner and more
The horizontal arrow is similar but involving $s$. The arrow $u$ in (6) is the adjunct of the map given by the diagonal of the pullback composed with the evaluation map,

$$a \otimes b \otimes [a, b'] \times_{[a \otimes b, \perp]} [b, a'] \to a \otimes b \otimes [a \otimes b, \perp] \xrightarrow{\text{ev}} \perp$$

The unit of the tensor product is $(i, \perp, \lambda_{\perp} : i \otimes \perp \to \perp)$. There is a dualising functor

$$\mathrm{Chu}(C, \perp)^{\mathrm{op}} \to \mathrm{Chu}(C, \perp) :: (a, a', r) \mapsto (a', a, r\sigma),$$

and together with the earlier tensor one can show that $\mathrm{Chu}(C, \perp)$ is $*$-autonomous [41], [42]. There is also an evident functor

$$C \to \mathrm{Chu}(C, \perp) :: a \mapsto (a, [a, \perp], \mathrm{ev})$$

which has a right adjoint given by the obvious forgetful functor.

It is known that the Chu construction is functorial $\mathrm{Chu}: \mathrm{CSMC}_{\perp} \to *\mathrm{Aut}$ where $\mathrm{CSMC}_{\perp}$ is the 2-category of closed symmetric monoidal categories with pullbacks and a specified object $\perp$ [43]. The morphisms are the lax monoidal functors $F: C \to D$ which laxly preserve the specified objects so that there exists an arrow $F(\perp_C) \to \perp_D$. The 2-cells are the natural isomorphisms. See [43] for the coherences that these data must satisfy.

**Remark 1:** The notion of $*$-functor in [43] does not include (4), though it is fairly straightforward to check that $\mathrm{Chu}(F)$ satisfies it for any functor $F$ in $\mathrm{CSMC}_{\perp}$.

Upon restricting to those CSMCs with pullbacks and pushouts, $\mathrm{Chu}$ is a right 2-adjoint to the forgetful functor $U$.

$$\mathrm{CSMC}_{\perp}^{\perp} \xrightarrow{\mathrm{Chu}}_{\leftarrow\leftarrow\leftarrow}^{\perp} \mathrm{Aut}^{\perp} \quad (7)$$

Here we restrict $*\mathrm{Aut}$ to just the $*$-autonomous categories with all pullbacks and only allow 2-cells that are isomorphisms.

Now we note a few useful properties of $\mathrm{Chu}$. Firstly, there is a sub-2-category $\mathrm{CSMC}_{N, \perp}^{\perp}$ given by restricting $\mathrm{CSMC}_{\perp}$ to the normal functors: those which, up to coherent isomorphism, preserve both the unit objects and the specified objects, $F(\perp_C) \cong \perp_D$. In this setting, $\mathrm{Chu}(F)$ is itself normal so that the adjunction (7) restricts to one involving $*\mathrm{Aut}_N$.

Additionally $\mathrm{Chu}$ behaves well with the monoidal structure of $\mathrm{CSMC}_{\perp}$.

**Proposition 1:** $\mathrm{Chu}$ is a strong monoidal 2-functor.

*Proof:* In Appendix A-C.

<figure><img src="image_8.png" /></figure>

### III. CONSTRUCTING BV-CATEGORIES

#### A. Duoidal Categories

Our starting point for constructing BV-categories will be a minimal model of the sequencing operator and its interaction with the tensor known as a duoidal category.

**Definition 6:** A $\otimes$-closed, $\otimes$-symmetric duoidal category $C$ is a pseudomonoid in CSMC, the monoidal 2-category of closed symmetric monoidal categories, lax monoidal functors and monoidal natural transformations.

This means that a $\otimes$-closed, $\otimes$-symmetric duoidal category $C$ is equipped with a closed symmetric monoidal structure

($\otimes$, $i_{\otimes}$), together with an additional tensor ($\otimes$, $i_{\otimes}$). These tensors interact via natural transformations of the following form,

$$(a \otimes b) \otimes (c \otimes d) \xrightarrow{\delta_{abcd}} (a \otimes c) \otimes (b \otimes d) \\ i_{\otimes} \xrightarrow{\gamma} i_{\otimes} \otimes i_{\otimes}, \quad i_{\otimes} \otimes i_{\otimes} \xrightarrow{\mu} i_{\otimes}, \quad i_{\otimes} \xrightarrow{\nu} i_{\otimes}$$

which must satisfy a series of coherence conditions which can be found in e.g. [49].

A duoidal category is normal when $i_{\otimes} \cong i_{\otimes}$. These are pseudomonoids in the monoidal 2-category CSMC$_N$.

**Definition 7:** There are monoidal 2-categories CSDuo and CSNDuo of $\otimes$-symmetric, $\otimes$-closed (normal) duoidal categories, lax-lax monoidal functors and monoidal natural transformations

#### B. BV-Categories

BV-categories were first defined in [39] and intended as minimal models of BV-logic [31]. Since BV-logic is an extension of MLL to incorporate the sequencing connective of Retoré [29], a BV-category $C$ is an extension of a $*$-autonomous one. We note that what we refer to as a BV-category is known as a BV-category with negation in [39].

A pre-BV-category is a $*$-autonomous category $C$ that is equipped with an additional monoidal structure ($\otimes$, $i_{\otimes}$) such that $(C, \otimes, \otimes)$ and $(C, \otimes, \mathcal{N})$ are both duoidal categories. Furthermore, there are natural isomorphisms making the $\otimes$ self-dual,

$$(a \otimes b)^* \cong a^* \otimes b^*, \quad i_{\otimes} \cong i_{\otimes}^*.$$

These data are required to interact coherently, for instance the duoidal interchange for ($\otimes$, $\mathcal{N}$) is the dual of that of ($\otimes$, $\otimes$), up to the self-duality of the $\otimes$. A pre-BV-category is a BV-category when $i_{\otimes} \cong i_{\otimes}$.

**Definition 8:** [39] A pre-BV-category (with negation) is a $*$-autonomous category with an additional monoidal structure ($\otimes$, $i_{\otimes}$) such that $- \otimes -$ is a degenerate linear functor and the associator $\alpha_{\otimes}$ is linear natural.

Using our equivalence between $*$-functors and degenerate linear functors on $*$-autonomous categories we can reframe BV-categories as algebraic objects.

**Theorem 2:** A pre-BV-category is a pseudomonoid in $*\mathrm{Aut}$ and a BV-category is a pseudomonoid in $*\mathrm{Aut}_N$.

*Proof:* In Appendix A-D.

<figure><img src="image_9.png" /></figure>

**Remark 2:** It should be noted that our definition of pre-BV-category appears to be slightly stronger than that of [39] since there they do not ask for any constraints on the unit object $i_{\otimes}$. In our setting, it makes sense to demand that the functor $i_{\otimes}: 1 \to C$ giving the unit in the pseudomonoid is itself a $*$-functor, and thus degenerate linear. The consequence of this is to give us the maps $\mu$ and $\nu$ of the duoidal structure, plus their coherence. This in turn gives a mixator $i_{\otimes} \xrightarrow{\nu} i_{\otimes} \cong i_{\otimes}^* \xrightarrow{\nu^*} i_{\otimes}^*$ so that any pre-BV-category is mix. In the case of a BV-category $i_{\otimes} \cong i_{\otimes}$ implies the category is isomix.

With this abstraction of (pre-)BV-categories in place, there are obvious candidates for the higher cells between them.
**Definition 9:** A pre-BV-functor is a pseudomonoid homomorphism in *Aut and pre-BV-transformation is an intertwiner of pseudomonoid homomorphisms in *Aut. BV-functors and BV-transformations are defined analogously but in *AutN. These structures assemble into monoidal 2-categories pre-BV and BV.

Explicitly, a pre-BV-functor $F: C \to \mathcal{D}$ consists of a $*$-functor $F$ equipped with $*$-natural transformations $F(-) \otimes F(-) \Rightarrow F(- \otimes -)$ and $i_{\mathcal{D}}^{\mathcal{C}} \to F(i_{\mathcal{D}}^{\mathcal{C}})$. The coherences are those of a lax-lax duoidal functor (see e.g. [49]) with additional compatibility with the $*$. This means that not only is $F$ laxly $\otimes$-monoidal it is also laxly $\otimes$-monoidal in a compatible fashion.

### C. Constructing BV-Categories via the Chu Construction

**Theorem 3:** Let $C$ be a $\otimes$-closed, $\otimes$-symmetric duoidal category with all pullbacks and a chosen object $\perp$ which is a $\otimes$-monoid. Then $\mathrm{Chu}(C, \perp)$ is a pre-BV-category and there is a $2$-functor,

$$ \mathrm{Chu}: \mathrm{CSDuo}_{\perp}^{\perp} \to \mathrm{pre-BV}. $$

*Proof:* In Appendix A-E.

One canonical choice of $\perp$ in the context of the previous theorem is the unit object for the sequencing tensor $i_{\otimes}$. Since this is trivially a $\otimes$-monoid, $\mathrm{Chu}(C, i_{\otimes})$ is always a pre-BV-category.

**Theorem 4:** Let $C$ be a $\otimes$-closed, $\otimes$-symmetric normal duoidal category with all pullbacks. Then $\mathrm{Chu}(C, i_{\otimes})$ is a BV-category and there is a $2$-functor,

$$ \mathrm{Chu}: \mathrm{CSNDuo}^{\perp} \to \mathrm{BV}. $$

*Proof:* In Appendix A-F.

**Theorem 5:** The Chu construction is cofree from duoidal to BV-categories. More precisely, upon restricting to BV-categories with pullbacks and pushouts, Chu is a right $2$-adjoint to the forgetful functor from BV-categories to $\otimes$-closed $\otimes$-symmetric normal duoidal categories.

$$ \mathrm{CSDuo}_{\perp}^{\perp} \xrightarrow[\frac{T}{U}]{\mathrm{Chu}} \mathrm{pre-BV}^{\perp} $$

$$ \mathrm{CSNDuo}^{\perp} \xrightarrow[\frac{T}{U}]{\mathrm{Chu}} \mathrm{BV}^{\perp} $$

*Proof:* The functor $\mathrm{Chu}: \mathrm{CSMC}_{\perp}^{\perp} \to *\mathrm{Aut}$ is a right adjoint in Mon2Cat to the forgetful functor $U$ from $*$-autonomous categories to closed symmetric monoidal categories (see (7) and [43]). From [50] the assignment PsMon lifts to a $2$-functor PsMon: Mon2Cat $\to$ 2Cat. Since $2$-functors preserve adjunctions, it follows that PsMon($\mathrm{Chu}$) is right-adjoint to PsMon($U$).

Let us now endeavour to unpack the content of Theorems 3 and 4 to better understand the (pre-)BV structure of $\mathrm{Chu}(C, \perp)$.

The tensor $\otimes$ of $\mathrm{Chu}(C, \perp)$ lifted from that of $C$ acts on objects as,

$$ (a, a', r) \otimes (b, b', s) = (a \otimes b, a' \otimes b', m(r \otimes s)\delta) $$

where the final component is the following arrow

$$ (a \otimes b) \otimes (a' \otimes b') \xrightarrow{\delta} (a \otimes a') \otimes (b \otimes b') \xrightarrow{r \otimes s} \perp \otimes \perp \xrightarrow{m} \perp $$

obtained from composing the duoidal distributor from $C$ with $r$ and $s$, and the multiplication $m$ on the chosen dualising object $\perp$. The unit object is $(i_{\otimes}, i_{\otimes}, i_{\otimes} \otimes i_{\otimes} \xrightarrow{\mu} i_{\otimes} \xrightarrow{u} \perp)$ where $u$ is the unit of the $\otimes$-monoid structure on $\perp$.

In the case that $C$ is normal so that $\mathrm{Chu}(C, i_{\otimes})$ is BV, the unit object of $\otimes$ is $(i_{\otimes}, i_{\otimes}, i_{\otimes} \otimes i_{\otimes} \cong i_{\otimes})$ which coincides up to isomorphism with the units of $\otimes$ and $\mathcal{R}$, as expected.

We can prove explicitly that the sequencing operator is strictly self dual.

**Proposition 2:** Under the assumptions of Theorem 3 or 4, the sequencing operator of $\mathrm{Chu}(C, \perp)$ is self dual so that $((a, a', r) \otimes (b, b', s))^* = (a, a', r)^* \otimes (b, b', s)^*$.

*Proof:*

$$ \begin{aligned} ((a, a', r) \otimes (b, b', s))^* &= (a \otimes b, a' \otimes b', m(r \otimes s)\delta)^* \\ &= (a' \otimes b', a \otimes b, m(r \otimes s)\delta\sigma) \\ &= (a' \otimes b', a \otimes b, m(r\sigma \otimes s\sigma)\delta) \\ &= (a', a, r\sigma) \otimes (b', b, s\sigma) \\ &= (a, a', r)^* \otimes (b, b', s)^* \end{aligned} \quad \blacksquare $$

The duoidal distributors between $\otimes$ and $\otimes$ and between $\otimes$ and $\mathcal{R}$ are given by lifting $\delta$ from $C$. Writing $\mathfrak{a} = (a, a', r)$ for an object of $\mathrm{Chu}(C, \perp)$, there are distributors

$$ (\mathfrak{a} \otimes \mathfrak{b}) \otimes (\mathfrak{c} \otimes \mathfrak{d}) \xrightarrow{\delta_{\mathfrak{abc}\mathfrak{d}}} (\mathfrak{a} \otimes \mathfrak{c}) \otimes (\mathfrak{b} \otimes \mathfrak{d}) \quad (8) $$

$$ (\mathfrak{a} \otimes \mathfrak{b}) \otimes (\mathfrak{c} \otimes \mathfrak{d}) \xrightarrow{\varepsilon_{\mathfrak{abc}\mathfrak{d}}} (\mathfrak{a} \otimes \mathfrak{c}) \otimes \mathfrak{R} (\mathfrak{b} \otimes \mathfrak{d}) \quad (9) $$

To describe the former explicitly we calculate,

$$ \begin{aligned} (\mathfrak{a} \otimes \mathfrak{b}) \otimes (\mathfrak{c} \otimes \mathfrak{d}) &= (ab, a'b') \otimes (cd, c'd') \\ &= (ab \otimes cd, [ab, c'd'] \times_{[ab \otimes cd, \perp]} [cd, a'b']) \end{aligned} $$

where to save space we have suppressed $\otimes$ by writing it as concatenation and neglected the final components involving $r$ and $s$. On the other hand,

$$ \begin{aligned} (\mathfrak{a} \otimes \mathfrak{c}) \otimes (\mathfrak{b} \otimes \mathfrak{d}) &= (a \otimes c, [a, c'] \times_p [c, a']) \otimes (b \otimes d, [b, d'] \times_p [d, b']) \\ &= ((a \otimes c)(b \otimes d), ([a, c'] \times_p [c, a'])([b, d'] \times_p [d, b])) \end{aligned} $$

where $\times_p$ denotes the pullback.

Hence we see that the first component of (8) is given by $\delta_{abcd}$ from $C$. The second component is more involved and the desired arrow can be constructed with some diagram chasing. See Appendix A-A for more details. The distributor (9) is given by dualising (8).

### D. Adding Additives

When $C$ is complete and cocomplete, $\mathrm{Chu}(C, \perp)$ is too with,

$$ \lim_i (a_i, a'_i, r_i) = (\lim_i a_i, \lim_i a'_i, r) $$

$$ \lim_i (a_i, a'_i, r_i) = (\lim_i a_i, \lim_i a'_i, r) $$

where in the first case $r$ is given by uncurrying $\lim_i a_i \to \lim_i [a'_i, \perp] \cong [\lim_i a'_i, \perp]$, and similarly for the latter. Thus when $C$ has products and coproducts so does $\mathrm{Chu}(C, \perp)$ and in the setting of Theorem 3 or 4, is moreover a (pre-)BV-category with additives. We suggest calling these (pre-)MAV-categories as they are candidates for models of MAV-logic [51].
# IV. STRONG PROFUNCTORS, INTERVENTIONS AND CONTEXTS

## A. Interventions

In this section we will introduce the mathematical tools that we will use to model contexts and interventions of agents in spacetime. Let us start with the notion of a profunctor.

**Definition 10:** Let $\mathcal{C}$ and $\mathcal{D}$ be categories. A profunctor $P: \mathcal{C} \to \mathcal{D}$ is a functor $\mathcal{D}^{\mathrm{op}} \times \mathcal{C} \to \mathrm{Set}$.

A profunctor $P$ is an assignment of a family of sets $P(d, c)$ over a pair of categories, such that they vary covariantly in $\mathcal{C}$ and contravariantly in $\mathcal{D}$. They are also known as bimodules: the family of sets has a left action by $\mathcal{D}$ and a right action by $\mathcal{C}$, analogously to bimodules between rings.

In physical terms, a profunctor represents a basic model for a space which can be probed. The contravariant variable represents the possibility to make a choice, while the covariant variable represents the possibility to observe some outcome. The sets $P(d, c)$ consist of all the possible interventions by the agent. We visualise $P$ as on the left of (10).

<figure><img src="image_10.png" /></figure>

An example of an intervention $P$ is drawn on the right of (10). Explicitly this is the profunctor $\mathcal{C}_\alpha := \mathcal{C}(a \otimes -, a' \otimes =)$, which contains for any $(x, x')$ the set of bipartite processes $\phi: a \otimes x \to a' \otimes x'$. We can think of the fixed $\alpha := (a, a')$ as the type of the device that the agent can probe and the variable $x := (x, x')$ as all the possible choices $x$ and outcomes $x'$ the agent can probe $\alpha$ with. We will meet other forms of intervention later.

For the applications in this work we will only need to consider endoprofunctors $P: \mathcal{C} \to \mathcal{C}$ on some given monoidal category $\mathcal{C}$, which together with the natural transformations between them form a category $\mathrm{Prof}(\mathcal{C})$. This category has two tensors, the first is given by composing the profunctors in the direction of composition in $\mathcal{C}$,

$$ (P \otimes Q)(-, -) := \int^{c} P(-, c) \times Q(c, -), $$

using a special type of colimit known as a coend [52]. We can visualise $\otimes$ as connecting the output of $P$ into the input of $Q$, as in the left-hand diagram below.

<figure><img src="image_11.png" /></figure>

The coend is analogous to the tensor product of bimodules: it acts to quotient the product by the action of $\mathcal{C}$ on the right of $P$ and the left of $Q$. Physically, this means we can slide local maps between the two labs as in the right-hand diagram above. The tensor product $\otimes$ has the hom-profunctor $1_{\mathcal{C}} = \mathcal{C}(-, -)$ as its unit object.

$$ 1_{\mathcal{C}} \cong \text{[Diagram]} $$

This is the space where an agent performs some trivial intervention by not interacting with the probe.

The second monoidal structure of $\mathrm{Prof}(\mathcal{C})$ is given by Day convolution [53], [54] over the monoidal structure of $\mathcal{C}$,

$$ (P \otimes Q)(-, -) := \int^{aa'bb'} \mathcal{C}(-, a \otimes b) \times P(a, a') \times Q(b, b') \times \mathcal{C}(a' \otimes b', -) $$

which has unit object $y_i \times y^i = \mathcal{C}(-, i) \times \mathcal{C}(i, -)$. We can think of $P \otimes Q$ as the space of separable interventions by the two agents as depicted below.

<figure><img src="image_12.png" /></figure>

The tensors $(\otimes, y_i \times y^i)$ and $(\otimes, 1_{\mathcal{C}})$ make $\mathrm{Prof}(\mathcal{C})$ a $\otimes$-closed duoidal category [36], [37].

**1) Monoidal Interventions:** The model of interventions as profunctors presented so far is lacking one key feature: compatibility between the interventions and the monoidal structure of $\mathcal{C}$. This is captured by the notion of a strong profunctor also known as a Tambara module.

**Definition 11:** Let $\mathcal{C}$ be a symmetric monoidal category. An endoprofunctor $P: \mathcal{C} \to \mathcal{C}$ is strong when it is equipped with a family of natural transformations

$$ \zeta_{abcd} : \mathcal{C}(a, b) \times P(c, d) \to P(a \otimes c, b \otimes d) $$

such that a series of coherence conditions hold making these natural transformations essentially associative and unital [55], [56].

Strong profunctors are those which have not only actions by $\mathcal{C}$ in the “vertical” direction of composition, but also actions by $\mathcal{C}$ in the “horizontal” direction of the tensor product. We can therefore think of them as bimodules in both dimensions simultaneously and compatibly. From a physical perspective, the strength of $P$ means that if one agent is probing $P$ and
another is performing trivial interventions, then there is an arrow mapping the agents into the same lab.

<figure><img src="image_13.png" /></figure>

This witnesses the fact that the collection of interventions that can be performed by only one agent using device P are strictly weaker than those that can be performed if both agents had access to P.

The natural transformations between profunctors can be straightforwardly specialised to play well with strengths.

**Definition 12:** Let $P$ and $Q$ be strong endoprofunctors on a symmetric monoidal category $C$. A natural transformation $\eta: P \Rightarrow Q$ is strong when it commutes with the strengths,

$$ \begin{array}{ccc} C(a, b) \times P(c, d) & \xrightarrow{\zeta_{abcd}^P} & P(a \otimes c, b \otimes d) \\ \multicolumn{1}{c}{\xrightarrow{1 \times \eta_{cd}}} & & \multicolumn{1}{c}{\xrightarrow{\eta_{a \otimes c, b \otimes d}}} \\ C(a, b) \times Q(c, d) & \xrightarrow{\zeta_{abcd}^Q} & Q(a \otimes c, b \otimes d) \end{array} $$

Strong endoprofunctors on $C$ and strong natural transformations assemble into a category $\text{StProf}(C)$. This category inherits the tensors of $\text{Prof}(C)$. $(\otimes, 1_C)$ becomes a tensor by equipping $P \otimes Q$ with a canonical strength induced by those of $P$ and $Q$. The other tensor product, which we will also denote by $\otimes$, arises by a quotient of that of $\text{Prof}(C)$ to turn it into a bimodular tensor but in the direction of the tensor product of $C$. See [22], [36], [37] for further discussion of this. The unit object for this tensor is now $1_C$ witnessing the fact that,

<figure><img src="image_14.png" /></figure>

Altogether, $\text{StProf}(C)$ is a $\otimes$-closed, normal duoidal category when equipped with $(\otimes, 1_C)$ and $(\otimes, 1_C)$ [36], [37].

## B. Contexts

Thus far we have seen how strong endoprofunctors provide a model of interventions by agents. It turns out we can also use $\text{StProf}(C)$ to model the dual picture, that of the spacetime contexts surrounding the agents. Rather than imagining $P$ as the intervention in equation (10) we suppose $P$ takes the following form.

<figure><img src="image_15.png" /></figure>

It is worth noticing that in this dual view, the roles of the green probing arrows and the black wires have reversed, with the former now fixed and the latter varying over the categories.

Examples of strong endoprofunctors of this form arise from the following category of *coend optics* [56].

**Definition 13:** Let $(C, \otimes, i)$ be a symmetric monoidal category. The category $\text{Optic}(C)$ has objects given by pairs $\mathbf{a} := (a, a')$ of objects of $C$. The homs are given by the following sets,

$$ \text{Optic}(C)(\mathbf{a}, \mathbf{b}) := \int^{x} C(b, x \otimes \mathbf{a}) \times C(x \otimes \mathbf{a}', \mathbf{b}'). $$

The category $\text{Optic}(C)$ has morphisms given by the single-holed combs built from morphisms of $C$.

<figure><img src="image_16.png" /></figure>

Explicitly, a morphism $\mathbf{a} \to \mathbf{b}$ is given by an equivalence class $(f, g)$ of pairs of maps $f: b \to x \otimes a$ and $g: x \otimes a' \to b'$ for some $x$, quotiented by the equivalence relation generated by sliding morphisms between the two halves of the comb.

It turns out that strong endoprofunctors are the copresheaf category of coend optics, $\text{StProf}(C) \cong [\text{Optic}(C), \text{Set}]$ [56]. In particular, the Yoneda embedding $y: \text{Optic}(C) \to \text{StProf}(C)$ sends $\mathbf{a}$ to $y_{\mathbf{a}}$ which is the set of all optics with $\mathbf{a}$ as input. We can think of this as a “hole” at $\mathbf{a}$ in the string diagrams of $C$. In other words $y_{\mathbf{a}}$ is a strong endoprofunctor modelling contexts of type $\mathbf{a}$. These contexts have a special form, in that they all decompose in terms of maps from $C$. There exist strong profunctors which can model generalised contexts including quantum supermaps such as the quantum switch [22]. Some of these will be discussed in more detail in the next section.

## C. Duality Between Interventions and Contexts

Since $\text{StProf}(C)$ is $\otimes$-closed, there is a weak dualising functor $(-)^* := [-, 1]$. In [22] it was pointed out that this dualising functor behaves as $y_{\mathbf{a}}^* \cong C_{\mathbf{a}} := C(a \otimes -, a' \otimes =)$, sending the optic context at $\mathbf{a}$ to the set of interventions at $\mathbf{a}$. This gives a partial duality between these simple types of contexts and inventions, but note that generally $C_{\mathbf{a}}^* \not\cong y_{\mathbf{a}}$.

The failure of $P^{**} \cong P$ in $\text{StProf}(C)$ (even for the most important interventions $C_{\mathbf{a}}$ and contexts $y_{\mathbf{a}}$) means that there is no hope of this category being *-autonomous or indeed BV. This prevents it from being a fully fledged model of spacetime events over $C$. We will see in the next section that by uniting interventions and contexts, it is possible to rectify this problem.

# V. SPACETIME EVENTS VIA THE STRONG HYLAND ENVELOPE

## A. The Strong Hyland Envelope

Hyland [44] and later Shulman [45] describe a category dubbed the *Hyland envelope* in the latter, which involves taking the Chu construction of the category of endoprofunctors
over some given category $\mathcal{C}$. They present this at the level of polycategories, but it will suffice to just consider its standard categorical analogue.

**Definition 14 (Hyland Envelope):**

$$ \mathrm{Env}(\mathcal{C}) := \mathrm{Chu}(\mathrm{Prof}(\mathcal{C}), 1_c) $$

Note that $\mathrm{Prof}(\mathcal{C})$ is $\otimes$-closed monoidal and being a presheaf category has all pullbacks so that $\mathrm{Env}(\mathcal{C})$ is well defined. Also note that $1_c$ is the unit of $\otimes$ so it is trivially a $\otimes$-monoid. Therefore, by Theorem 3, $\mathrm{Env}(\mathcal{C})$ is a pre-BV-category.

We can adjust the Hyland envelope to be better suited to our intended goals of modelling spacetime events by replacing profunctors with their strong counterparts.

**Definition 15 (Strong Hyland Envelope):**

$$ \mathrm{StEnv}(\mathcal{C}) := \mathrm{Chu}(\mathrm{StProf}(\mathcal{C}), 1_c) $$

Since $\mathrm{StProf}(\mathcal{C})$ is normal duoidal, $\mathrm{StEnv}(\mathcal{C})$ is a BV-category by Theorem 4.

## B. Intervention-Context Pairs

A Chu space $(P, P', \eta)$ in $\mathrm{StEnv}(\mathcal{C})$ consists of a pair of strong endoprofunctors $P$ and $P'$ and a strong natural transformation $\eta: P \otimes P' \to 1$. We can think of $P$ as the intervention and $P'$ as the context, with $\eta$ giving a specified way of evaluating the context on the intervention, so that an object looks like the following.

<figure><img src="image_17.png" /></figure>

## C. Basic Events

We can embed essentially all of the important structure from strong endoprofunctors into the strong envelope via the canonical functor,

$$ \mathrm{StProf}(\mathcal{C}) \to \mathrm{StEnv}(\mathcal{C}) :: P \mapsto (P, P^*, \mathrm{ev}). \quad (11) $$

On the intervention $C_a$ we get the object,

$$ (C_a, C_a^*, \mathrm{ev}) = \left( \begin{array}{c} \text{[Diagram of a category with an arrow from $a'$ to $a$]} \\ \text{[Diagram of a category with an arrow from $a$ to $a'$]} \end{array} \right) \quad (12) $$

which pairs the concrete intervention $C_a$ with the abstract context $C_a^*$. The latter was studied in [22] and shown to be the space of all single-party black-box supermaps on $a$.

**Definition 16:** We call the object (12) an *event* at $a$.

From now on whenever we consider events we will neglect the evaluation morphisms $\mathrm{ev}$ and leave it to the faith of the reader that those parts do indeed work out.

The functor (11) is always strong $\otimes$-monoidal so that,

$$ (C_a, C_a^*) \otimes (C_b, C_b^*) \cong (C_a \otimes C_b, (C_a \otimes C_b)^*), $$

essentially recovering the tensor from $\mathrm{StProf}(\mathcal{C})$. The intervention consists of the separable maps between $a$ and $b$ [22], while the context consists of all joint contexts on $a$ and $b$ that when partially evaluated in one input return a valid context on the other input.

The behaviour of the sequencing operator on events also essentially recovers that from $\mathrm{StProf}(\mathcal{C})$. From the definition, $(C_a, C_a^*) \otimes (C_b, C_b^*) = (C_a \otimes C_b, C_a^* \otimes C_b^*)$. Here, the intervention is the sequential composition of the basic interventions at $a$ and $b$. Similarly, the context consists of the sequential composition of all valid single-party contexts on the two parties.

Let us now consider the new connective we have accessible to us, the $\mathcal{N}$. Routine calculation shows,

$$ (C_a, C_a^*) \mathcal{N} (C_b, C_b^*) = ([C_a^*, C_b] \times_{[C_a^* \otimes C_b^*, 1]} [C_b^*, C_a]), C_a^* \otimes C_b^*) $$

The context here is the easiest to interpret: it consists of the space of single-party contexts with shared past and future. As for the intervention, we can place bounds on it. Firstly, for any Chu spaces $P = (P, P')$ and $Q = (Q, Q')$ the following diagram commutes,

<figure><img src="image_18.png" /></figure>

where the $\tau$ are the canonical embeddings coming from the BV structure and the object in the centre is the pushout. Taking $P$ and $Q$ to be events gives an arrow,

$$ (C_a \otimes C_b) \vee (C_b \otimes C_a) \to [C_a^*, C_b] \times_{[C_a^* \otimes C_b^*, 1]} [C_b^*, C_a] $$

from the join of the semi-localisable maps with $a$ and $b$ in either causal order into the intervention in the $\mathcal{N}$ of events.

On the other hand, there is also an arrow

$$ [C_a^*, C_b] \times_{[C_a^* \otimes C_b^*, 1]} [C_b^*, C_a] \to [C_a^* \otimes C_b^*, 1] \to C_a \otimes b \quad (13) $$

where the first arrow is the diagonal of the pullback. Noting that $C_a \otimes b \cong y_{a \otimes b}^*$, the second arrow of (13) is the adjunct to,

$$ y_a \otimes y_b \otimes [y_a^{**} \otimes y_b^{**}, 1] \to y_a^{**} \otimes y_b^{**} \otimes [y_a^{**} \otimes y_b^{**}, 1] \xrightarrow{\mathrm{ev}} 1 $$

So we see that the intervention in the $\mathcal{N}$ of events is bounded below by the join of semi-localisable maps on $a$ and $b$ and bounded above by the space of all bipartite maps on $a$ and $b$.

The functor (11) is also fully faithful which allows us to recover all the higher-order transformations present in $\mathrm{StProf}(\mathcal{C})$. For instance, a single-party higher-order map is an arrow of the form, $(C_a, C_a^*) \to (C_b, C_b^*)$ which in turn is comprised of a pair of strong natural transformations $S: C_a \to C_b$ and $S': C_b^* \to C_a^*$. $S'$ is actually determined by $S$ since diagram (5) must commute.
## D. First-Order Maps

While the main focus of this article is on developing BV-logical models of spacetime interventions and higher-order processes, it is worth remarking on how the first-order maps appear in the strong Hyland envelope.

Since we interpret the object **a** as the intervention at $(a, a')$ in $\mathcal{C}$, as a special case we can consider objects of the form and $(i, a)$ and lift these to $\text{StEnv}(\mathcal{C})$.

**Definition 17:** An event is first-order if its carrying object is of the form $(i, a)$. Such events always take the form,

$$(\mathcal{C}(-, a \otimes -), \mathcal{C}(a \otimes -, -), \text{ev}) \cong (y_{a,i}, y_{i,a}, \text{ev}),$$

because $y_{ai} \cong C_{ia} \cong y_{ia}^* \cong C_{ai}^*$ and $y_{ai}^* \cong C_{ia}^* \cong y_{ia} \cong C_{ai}$. Note that first-order events are always causally faithful.

An arrow between first-order events,

$$(\mathcal{C}(-, a \otimes -), \mathcal{C}(a \otimes -, -)) \to (\mathcal{C}(-, b \otimes -), \mathcal{C}(b \otimes -, -))$$

is characterised immediately by the Yoneda lemma as a morphism $a \to b$ in $\mathcal{C}$ and is therefore a first-order transformation.

First-order events are somewhat special with regards to the tensor, the sequencing operator and the par.

**Lemma 1:** First-order systems are closed under $\otimes$, $\otimes$ and $\mathcal{Y}$. Furthermore, if $P$ and $Q$ are first-order systems then $P\mathcal{Y}Q \cong P \otimes Q \cong P \otimes Q$.

*Proof:* Immediate by earlier results. ■

<figure><img src="image_19.png" /></figure>

So far what we have outlined is the abstract sense in which the strong Hyland envelope captures key concepts in the study of causal structure and abstract spacetime events. One might wonder what the direct connection to the foundations of physics is, and there are two answers to this question. The first, is to simply note that since (11) is a strong monoidal embedding of the category of strong endoprofunctors, results directly connecting strong profunctors to quantum supermaps are directly transferred. More precisely, arrows of the type $S : \mathcal{C}_a \to \mathcal{C}_b$ in the category of strong endoprofunctors were considered in [15], [21], [22] and shown to recover the single-party quantum supermaps. This extends to multi-input supermaps and the study of indefinite causal order [5], [6]: the multi-partite supermaps of [22] can be recovered similarly by considering maps out of $\otimes$ and $\otimes$ products of objects of the form $\mathcal{C}_a$ in $\text{StProf}(\mathcal{C})$ and directly transferred to $\text{StEnv}(\mathcal{C})$.

This first answer simply tells us that what was previously quite a well behaved model for categorical quantum supermaps can be equipped with a par to form a model of BV-logic, generalising a previously established result which builds the same conclusion from a compact closed base [19]. In this sense the strong Hyland envelope has advantages in for instance, being immediately applicable to infinite dimensional systems. The second answer however, will show that the strong Hyland envelope is actually giving us much more than the category of strong endoprofunctors. New objects generated in this category have a direct interpretation in terms of local comb decompositions, which allows for the strong Hyland envelope to cope with important deficiencies in the naive strong profunctor model of [21].

## VI. LOCAL COMB DECOMPOSITIONS

One of the most natural properties one might expect of events is that given higher-order processes of type $C_a \to C_{a'}$ and $C_b \to C_{b'}$, one could construct a higher-order process of type $C_{a \otimes b} \to C_{a' \otimes b'}$. In the case of finite dimensional quantum theory this has been identified as a property of the $\mathcal{Y}$ of finite dimensional higher-order processes [19], [23].

Turning to $\text{StProf}(\mathcal{C})$, in the special case that $C_a^* \cong y_a$ for all **a** it is possible to partially define a $\mathcal{Y}$ which behaves in the desired fashion, but it cannot be extended to an associative and unital tensor on the entire category [22]. The isomorphism $C_a^* \cong y_a$ was observed to be equivalent to the claim that a category possesses decompositions for single-party supermaps. Indeed it holds for the category $\text{StProf}(\text{CPTP})$ witnessing this decomposition theorem for single-party higher-order transformations on finite dimensional quantum channels.

A more serious problem however, is that even over the category of finite dimensional unitary linear maps (which are of central importance in the study of quantum causal structure [12]), one can observe that there will be no isomorphism $C_a^* \cong y_a$, because there exist pathological non-linear homomorphisms on strong profunctors that cannot be made to interchange over the space $C_{a \otimes b}$ [21]. It turns out that there are objects in the strong Hyland envelope which encode a resolution to this problem.

**Definition 18:** A causally faithful event is an object of the form $(\mathcal{C}_a, y_a, \text{ev})$.

A causally faithful event, in comparison to an event, has a stronger notion of context: we demand that the only valid contexts are combs.

Since each causally faithful event $(\mathcal{C}_a, y_a)$, is dual to an object $(y_a, \mathcal{C}_a)$ in the image of the embedding (11), some of the properties of tensors of faithful events can, like for events, be seen to follow from the properties of the dualising functor and the embedding (11).

We will now unpack the concrete meaning of causally faithful events to demonstrate that they resolve the issue of the behaviour of the $\mathcal{Y}$. In doing so we will also have proven that one can embed unitary supermaps into the strong Hyland envelope over the unitaries.

1) **Tensor:** Firstly, consider the tensor product of causally faithful events,

$$(\mathcal{C}_a, y_a) \otimes (\mathcal{C}_b, y_b) = (\mathcal{C}_a \otimes \mathcal{C}_b, [\mathcal{C}_a, y_b] \times [\mathcal{C}_a \otimes \mathcal{C}_b, 1] [\mathcal{C}_b, y_a]).$$

The context here is quite an interesting object as it describes precisely the set of bipartite generalised contexts at **a** and **b** which decompose as optics upon evaluation in one of their inputs. We will write $\text{LC}_{a,b}$ for this context of “local combs”.

To see why we can think of $\text{LC}_{a,b}$ in this way, consider a map $S$ in $[\mathcal{C}_a, y_b](\mathcal{C})$. This consists of a strong natural transformation $S : \mathcal{C}_a \to y_b(- \otimes c)$ which takes interventions at **a** to the optic context at **b**. For instance, its component $S_x$ at $x$ acts as,
<figure><img src="image_20.png" /></figure>

We can conceptualise $S$ as a two-input black-box supermap which returns an optic at $b$ when partially evaluated at $a$.

<figure><img src="image_21.png" /></figure>

The internal hom $[C_a, y_b]$ contains all such supermaps, and similarly for $[C_b, y_a]$ with $a$ and $b$ exchanged. Therefore, by taking the pullback $LC_{a,b}$ we are ensured to get just those bipartite supermaps which decompose as a comb upon evaluation in either of their inputs.

The multi-partite case follows similarly: the iterated pullback appearing in the second component of a tensor product of many causally faithful events describes precisely the space of multi-partite supermaps which decompose locally as a comb.

2) **Par:** Now consider the $\mathcal{N}$ of causally faithful events.

**Lemma 2:** $(C_a, y_a) \mathcal{N} (C_b, y_b) \cong (C_{a \otimes b}, y_{a \otimes b})$.

**Proof:**

$$ (C_a, y_a) \mathcal{N} (C_b, y_b) = ((y_a, C_a) \otimes (y_b, C_b))^* \\ = (y_{a \otimes b}, [y_a, C_b] \times_{[y_a \otimes y_b, 1]} [y_b, C_a])^* $$

where the first component follows because the $\otimes$ tensor of representable presheaves is given by the tensor of the representatives. Now note we have $[y_a, C_b] \cong [y_a \otimes y_b, 1] \cong [y_b, C_a]$ so that all objects involved in the pullback are naturally isomorphic, and moreover, $[y_a \otimes y_b, 1] \cong [y_{a \otimes b}, 1] \cong C_{a \otimes b}$. Finally note that the arrows involved in the desired pullback are both isomorphisms so that the pullback is itself naturally isomorphic to $C_{a \otimes b}$.

So we see that the $\mathcal{N}$ of causally faithful events acts to send the spaces $C_a$ and $C_b$ of interventions at $a$ and $b$ to the space of interventions $C_{a \otimes b}$ on the bipartite space $a \otimes b$. It also deals with the contexts correctly, ensuring that the spaces of optics at $a$ and $b$ are combined into the space of all optics on the joint system $a \otimes b$. It is worth pointing out that in a category which possesses decompositions for single-party supermaps, the $\mathcal{N}$ of events of course coincides with the above and thus has a simpler expression than that given earlier.

3) **Sequencing:** It is immediate to see $(C_a, y_a) \otimes (C_b, y_b) \cong (C_a \otimes C_b, y_a \otimes y_b)$. What is interesting here is the context, $y_a \otimes y_b$ which is precisely the space of two-input combs. This ensures that sequentially composed causally faithful events still possess a causally faithful context.

4) **Higher-Order Transformations:** We now turn our attention to the maps between causally faithful events. Starting with the single-party case, suppose we have an arrow $(S, S') : (C_a, y_a) \to (C_b, y_b)$ consisting of two strong natural transformations $S : C_a \to C_b$ and $S' : y_b \to y_a$ such that the diagram (5) commutes. $S$ is of the form of a single-party supermap from [22] but the compatibility of $S$ with $S'$ by (5) places extra demands of the form of this supermap. In fact, $S'$ can be immediately characterised by the Yoneda lemma and is given by an optic $a \to b$. Since diagram (5) must commute, it is therefore necessary that $S$ be given by the action of an optic on $C_a$. So we see that all single-party supermaps in $\text{StEnv}(C)$ possess a causally faithful decomposition as an optic.

The multi-partite supermaps between causally faithful events can be characterised similarly. For instance, an arrow $(S, S') : (C_a, y_a) \otimes (C_b, y_b) \to (C_c, y_c)$ consists of a pair of natural transformations $S : C_a \otimes C_b \to C_c$ and $S' : y_c \to LC_{a,b}$. $S$ is a bipartite supermap from [22] but $S'$ is characterised by the Yoneda lemma as an element of $LC_{a,b}(c)$. Since (5) must commute, we see that the higher-order transformation $(S, S')$ is a supermap possessing a local decomposition as a comb.

Similarly, $(S, S') : (C_a \otimes C_b, y_a \otimes y_b) \to (C_c, y_c)$ consists of a pair of strong natural transformations, $S : C_a \otimes C_b \to C_c$ and $S' : y_c \to y_a \otimes y_b$. The former is the same as a bipartite causally ordered supermap from [22] while $S'$ is characterised by the Yoneda lemma as an element of $(y_a \otimes y_b)(c)$ which is precisely the space of two-holed optics with inputs $a$ and $b$ and output $c$. Since (5) must commute, $S$ is characterised by the action of $S'$ on $C_a \otimes C_b$.

5) **Super-unitaries:** The previous discussion outlines a proof that the polycategory uQS of super-unitaries [21] embeds fully and faithfully into the model developed here. These unitary-preserving supermaps have very concrete representations in the one and two-input settings [57], are used for the purpose of quantum causal modelling [12], and are conjectured to have concrete graph-theoretic characterisations for arbitrarily many inputs [58].

**Definition 19:** The symmetric polycategory uQS has objects given by pairs of finite dimensional Hilbert spaces $H = (H, H')$ and polymorphisms $S : H_1 \dots H_n \to K_1 \dots K_m$ given by the linear maps on the tensor product of those Hilbert spaces which send unitaries to unitaries. This means that for tensorially extended unitaries $U_i : H_i \otimes X_i \to H'_i \otimes X'_i$, $S$ returns a unitary $S(\otimes_i U_i) : \otimes_i (K_i \otimes X_i) \to \otimes_i (K'_i \otimes X'_i)$. See [21] for more details.

**Theorem 6:** There is a fully faithful embedding of symmetric polycategories $E : \text{uQS} \to \text{StEnv}(U)$ from the polycategory uQS of super-unitaries into the strong Hyland envelope over the category $U$ of finite dimensional unitaries.

**Proof:** In Appendix A-G.
In summary, the causally faithful objects of the strong Hyland envelope model the key concept of local comb de-composition. The existence of such objects is quite clarifying as it demonstrates that one may have to make a choice. On one hand, one can hold onto fully abstract spacetime contexts with events of the form $(C_a, C_a^*)$, with the sacrifice being that the $\aleph$ will not allow for simultaneous application of contexts to either half of a bipartite morphism as argued for in [21]. Instead the $\aleph$ models an abstraction of the notion of two-way communication. On the other hand, one may choose to study the more concrete objects $(C_a, y_a)$ in which contexts have local decompositions, in this case one is rewarded by a very well behaved $\aleph$ which *does* support simultaneous application of contexts to bipartite morphisms.

**Remark 3:** In [21] an alternative model slot is put forward, which holds onto partially abstract spacetime contexts by imposing bi-commutancy. The question of whether there are alternative objects within StEnv($C$) with this property is left as a topic for future work.

## VII. CONCLUSION

The strong Hyland envelope over a symmetric monoidal category gives a canonical and well-behaved model of higher-order processes over an arbitrary physical theory. This work came alongside a more abstract desire to canonically construct BV-categories, and we have demonstrated that the Chu construction can cofreely achieve this while also being physically well-motivated.

While we have provided evidence that the strong Hyland envelope could be a good categorical model for the study of causal order in modern quantum foundations—in particular in the characterisation of its morphisms in familiar physical settings, and the establishment of its spatio-temporal connectives—we feel we have barely scratched the surface.

Since our model can support arbitrary symmetric monoidal categories of first-order processes, we have a candidate model for higher-order processes and indefinite causal order scenarios which includes infinite dimensional quantum systems and generalised physical theories. Clear next steps involve characterising this model in those new domains to produce concrete models that are more easily wieldable by those without a strong categorical background.

More concretely, natural future lines of enquiry involve understanding whether recent proposals for extending the study of indefinite causal order to specific generalised physical theories (Box-world [13], and Hex-Square theory [14]) fit within the general categorical framework. The successful characterisation of the most basic kinds of supermaps over pure and mixed finite dimensional quantum theory should be a sign for optimism in this regard. For each generalised physical theory, the categorical framework then aims to give a stable position from which the fundamental limits on causal correlations in physical theories can be studied, likely in combination with device-independent frameworks for causal correlations and inequalities [6], [59]–[61]. The framework

might also be better understood if the classification of supermaps in quantum theory into subclasses can be abstracted to general monoidal categories, such subclasses include for instance quantum circuits with dynamical control of causal order [62], consistent circuits for indefinite causal order [58], and purifiable supermaps [63].

We can also wonder what other logical features might be present in StEnv($C$). For instance, the Caus-construction has been recently demonstrated to exhibit a richer logic based on graph types which extends BV [25]. It would be interesting to understand whether any of those logical features are present in the model here and whether any direct comparisons between Caus($C$) and StEnv($C$) can be made. The Caus-construction was also shown in [25] to be a model of pomset logic which is known to not be equivalent to BV [64]. The separating statement does not appear to be generally true in our framework and we leave deeper investigation of this to future work.

With regard to the connections between system BV and BV-categories, we would like to stress again that as far as we are aware, it has not been shown that BV-categories provide a definitive notion of a model of system BV. We hope that our reframing of the definition of BV-categories as higher algebraic objects alongside their functors and natural transformations will be useful in this endeavour. BV-categories can be seen as a categorification of the BV-algebras of [40] (as a special case of MAV-algebras). There it is shown that BV is sound for BV-algebras and complete for a semantics in terms of BV-frames. An important part of their proof is that the Chu construction can be used to send duoidal pomonoids to BV-pomonoids which Theorem 4 categorifies. It would be interesting to understand whether the remainder of the steps of their proof can be transferred over to achieve soundness and completeness results for semantics in terms of BV-categories.

Finally, we have only studied the explicit features of the Chu construction over categories of strong endoprofunctors. This leaves open the question of the interpretation of the construction over other duoidal categories, and leads us to wonder whether the construction could be of interest in developing models for purposes other than studying spacetime interventions.

## ACKNOWLEDGEMENTS

This work has been partially funded by the French National Research Agency (ANR) within the framework of “Plan France 2030”, under the research projects EPIQ ANR-22-PETQ-0007 and HQI-R&D ANR-22-PNCQ-0002. The contributions of MW were split between his time at UCL and at CentraleSupélec. While based at University College London, MW was funded by the Engineering and Physical Sciences Research Council [grant number EP/W524335/1]. The internal string “tube” diagrams were made using a package heavily inspired by that of [65], [66].

## REFERENCES

[1] B. Coecke and A. Kissinger, *Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning*. Cambridge University Press, 2017.
[2] G. Chiribella, G. M. D’Ariano, and P. Perinotti, “Probabilistic theories with purification,” *Phys. Rev. A*, vol. 81, p. 062348, 2010.

[3] S. Gogioso and C. M. Scandolo, “Categorical probabilistic theories,” *EPTCS*, vol. 266, pp. 367–385, 2018.

[4] B. Coecke and R. Lal, “Causal categories: Relativistically interacting processes,” *Found Phys*, vol. 43, pp. 458–501, 2013.

[5] G. Chiribella, G. M. D’Ariano, P. Perinotti, and B. Valiron, “Quantum computations without definite causal structure,” *Phys. Rev. A*, vol. 88, p. 022318, 2013.

[6] O. Oreshkov, F. Costa, and Č. Brukner, “Quantum correlations with no causal order,” *Nature Communications*, vol. 3, no. 1092, 2012.

[7] F. A. Pollock, C. Rodríguez-Rosario, T. Frauenheim, M. Paternostro, and K. Modi, “Non-markovian quantum processes: Complete framework and efficient characterization,” *Phys. Rev. A*, vol. 97, p. 012127, Jan 2018. [Online]. Available: https://link.aps.org/doi/10.1103/PhysRevA.97.012127

[8] G. Chiribella, G. M. D’Ariano, and P. Perinotti, “Transforming quantum operations: Quantum supermaps,” *EPL (Europhysics Letters)*, vol. 83, no. 3, p. 30004, 2008.

[9] ——, “Quantum circuit architecture,” *Physical Review Letters*, vol. 101, no. 6, p. 060401, 2008.

[10] ——, “Theoretical framework for quantum networks,” *Phys. Rev. A*, vol. 80, p. 022339, 2009.

[11] G. Chiribella, “Perfect discrimination of no-signalling channels via quantum superposition of causal structures,” *Phys. Rev. A*, vol. 86, p. 040301, 2012.

[12] J. Barrett, R. Lorenz, and O. Oreshkov, “Cyclic quantum causal models,” *Nature Communications*, vol. 12, p. 885, 2021. [Online]. Available: https://doi.org/10.1038/s41467-020-20456-x

[13] J. Bavaresco, Å. Baumeler, Y. Guryanova, and C. Budroni, “Indefinite causal order in boxworld theories,” 2024. [Online]. Available: https://arxiv.org/abs/2411.00951

[14] K. Sengupta, “Achieving maximal causal indefiniteness in a maximally nonlocal theory,” 2024. [Online]. Available: https://arxiv.org/abs/2411.04201

[15] M. Wilson, G. Chiribella, and A. Kissinger, “Quantum supermaps are characterized by locality,” 2022.

[16] N. Sakharwade and L. Hardy, “A diagrammatic language for the causaloid framework,” 2024. [Online]. Available: https://arxiv.org/abs/2407.01522

[17] Y. Chen, P. Wang, and Z. Wang, “Causality and duality in multipartite generalized probabilistic theories,” 2024. [Online]. Available: https://arxiv.org/abs/2411.03903

[18] A. Jenčová, “On the structure of higher order quantum maps,” *arXiv preprint arXiv:2411.09256*, 2024.

[19] A. Kissinger and S. Uijlen, “A categorical semantics for causal structure,” *Logical Methods in Computer Science*, vol. 15, 2019.

[20] W. Simmons and A. Kissinger, “Higher-Order Causal Theories Are Models of BV-Logic,” in *47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)*, ser. Leibniz International Proceedings in Informatics (LIPIcs), S. Szeider, R. Ganian, and A. Silva, Eds., vol. 241. Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022, pp. 80:1–80:14.

[21] M. Wilson and G. Chiribella, “Free polycategories for unitary supermaps of arbitrary dimension,” 2022.

[22] J. Hefford and M. Wilson, “A Profunctorial Semantics for Quantum Supermaps,” in *Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science*, ser. LICS '24. New York, NY, USA: Association for Computing Machinery, 2024.

[23] A. Bisio and P. Perinotti, “Theoretical framework for higher-order quantum theory,” *Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences*, vol. 475, no. 2225, p. 20180706, 2019. [Online]. Available: http://dx.doi.org/10.1098/rspa.2018.0706

[24] L. Apadula, A. Bisio, and P. Perinotti, “No-signalling constrains quantum computation with indefinite causal structure,” *Quantum*, vol. 8, p. 1241, Feb. 2024. [Online]. Available: https://doi.org/10.22331/q-2024-02-05-1241

[25] W. Simmons and A. Kissinger, “A complete logic for causal consistency,” 2024.

[26] M. Wilson and G. Chiribella, “A mathematical framework for transformations of physical processes,” 2023.

[27] ——, “Causality in higher order process theories,” in *Proceedings QPL 2021*, vol. 343. Open Publishing Association, 2021, pp. 265–300. [Online]. Available: http://dx.doi.org/10.4204/EPTCS.343.12

[28] T. Hoffreumon and O. Oreshkov, “Projective characterization of higher-order quantum transformations,” 2022.

[29] C. Retoré, “Pomset logic: A non-commutative extension of classical linear logic,” in *Typed Lambda Calculi and Applications*, 1997, pp. 300–318.

[30] ——, “Réseaux et séquents ordonnés,” Ph.D. dissertation, Université Paris-Diderot - Paris VII, 1993.

[31] A. Guglielmi, “A system of interaction and structure,” *ACM Transactions on Computational Logic*, vol. 8, no. 1, 2007.

[32] A. Guglielmi and L. Straßburger, “Non-commutativity and mell in the calculus of structures,” in *Computer Science Logic*, L. Fribourg, Ed., 2001, pp. 54–68.

[33] R. Blute, I. Ivanov, and P. Panangaden, “Discrete quantum causal dynamics,” *International Journal of Theoretical Physics*, vol. 42, pp. 2025–2041, 2003.

[34] R. F. Blute, A. Guglielmi, I. T. Ivanov, P. Panangaden, and L. Straßburger, *A Logical Basis for Quantum Evolution and Entanglement*, 2014, pp. 90–107.

[35] J.-Y. Girard, “Between logic and quantic: a tract,” *Linear logic in computer science*, vol. 316, p. 346, 2004.

[36] R. Garner and I. L. Franco, “Commutativity,” *Journal of Pure and Applied Algebra*, vol. 220, no. 5, pp. 1707–1751, 2016.

[37] M. Earnshaw, J. Hefford, and M. Román, “The produoidal algebra of process decomposition,” 2023.

[38] M. Román, “Monoidal context theory,” Ph.D. dissertation, Tallinn University of Technology, 2023.

[39] R. Blute, P. Panangaden, and S. Slavnov, “Deep inference and probabilistic coherence spaces,” *Applied Categorical Structures*, vol. 20, pp. 209–228, 2012.

[40] R. Atkey and W. Kokke, “A semantic proof of generalised cut elimination for deep inference,” *Electronic Notes in Theoretical Informatics and Computer Science*, vol. Volume 4 - Proceedings of MFPS XL, 2024.

[41] P.-H. Chu, “Constructing *-autonomous categories,” appendix to [42].

[42] M. Barr, “*-autonomous categories,” *Lecture Notes in Mathematics*, vol. 752, 1979.

[43] D. Pavlović, “Chu i: cofree equivalences, dualities and *-autonomous categories,” *Mathematical Structures in Computer Science*, vol. 7, no. 1, pp. 49–73, 1997.

[44] J. Hyland, “Proof theory in the abstract,” *Annals of Pure and Applied Logic*, vol. 114, no. 1, pp. 43–78, 2002.

[45] M. Shulman, “*-autonomous envelopes and conservativity,” *Electronic Proceedings in Theoretical Computer Science*, vol. 353, pp. 175–194, 2021.

[46] R. Seely, “Linear logic, *-autonomous categories and cofree coalgebras,” *Contemporary Mathematics*, vol. 92, 1989.

[47] J. Cockett and R. Seely, “Weakly distributive categories,” *Journal of Pure and Applied Algebra*, vol. 114, no. 2, pp. 133–173, 1997.

[48] ——, “Linearly distributive functors,” *Journal of Pure and Applied Algebra*, vol. 143, no. 1, pp. 155–203, 1999.

[49] S. M. Marcelo Aguiar, *Monoidal Functors, Species and Hopf Algebras*. CRM Monograph Series, 2010, vol. 29.

[50] R. B. B. Lucyshyn-Wright, “Relative symmetric monoidal closed categories i: Autoenrichment and change of base,” 2015. [Online]. Available: https://arxiv.org/abs/1507.02220

[51] R. Horne, “The consistency and complexity of multiplicative additive system virtual,” *Scientific Annals of Computer Science*, vol. 25, no. 2, 2015.

[52] F. Loregian, (*Co*)end Calculus, ser. London Mathematical Society Lecture Note Series. Cambridge University Press, 2021.

[53] B. Day, “On closed categories of functors,” in *Reports of the Midwest Category Seminar IV*, vol. 137. Berlin, Heidelberg: Springer Berlin Heidelberg, 1970, pp. 1–38.

[54] ——, “Construction of biclosed categories,” Ph.D. dissertation, University of New South Wales, 1970.

[55] D. Tambara, “Distributors on a tensor category,” *Hokkaido Mathematical Journal*, vol. 35, no. 2, pp. 379 – 425, 2006.

[56] C. Pastro and R. Street, “Doubles for monoidal categories,” *Theory and Applications of Categories*, vol. 21, no. 4, pp. 61–75, 2008.

[57] W. Yokojima, M. T. Quintino, A. Soeda, and M. Murao, “Consequences of preserving reversibility in quantum superchannels,” *Quantum*, vol. 5, p. 441, Apr. 2021. [Online]. Available: https://doi.org/10.22331/q-2021-04-26-441
[58] A. Vanrietvelde, N. Ormrod, H. Kristjánsson, and J. Barrett, “Consistent circuits for indefinite causal order,” 2023. [Online].
Available: https://arxiv.org/abs/2206.10042

[59] T. van der Lugt, J. Barrett, and G. Chirabella, “Device-independent certification of indefinite causal order in the quantum switch,” 2023. [Online]. Available: https://arxiv.org/abs/2208.00719

[60] S. Gogioso and N. Pinzani, “The geometry of causality,” 2023. [Online]. Available: https://arxiv.org/abs/2303.09017

[61] ——, “The topology of causality,” 2023. [Online]. Available: https://arxiv.org/abs/2303.07148

[62] J. Wechs, H. Dourdent, A. A. Abbott, and C. Branciard, “Quantum circuits with classical versus quantum control of causal order,” PRX Quantum, vol. 2, p. 030335, 2021.

[63] M. Araújo, A. Feix, M. Navascués, and Č. Brukner, “A purification postulate for quantum mechanics with indefinite causal order,” Quantum, vol. 1, p. 10, Apr. 2017. [Online]. Available: https://doi.org/10.22331/q-2017-04-26-10

[64] L. T. D. Nguyen and L. Straßburger, “BV and Pomset Logic Are Not the Same,” in 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), vol. 216, 2022, pp. 32:1–32:17.

[65] B. Bartlett, C. L. Douglas, C. J. Schommer-Pries, and J. Vicary, “Extended 3-dimensional bordism as the theory of modular objects,” 2014.

[66] ——, “Modular categories as representations of the 3-dimensional bordism 2-category,” 2015.

[67] B. Day and R. Street, “Monoidal bicategories and hopf algebroids,” Advances in Mathematics, vol. 129, no. 1, pp. 99–157, 1997.

[68] P. McCrudden, “Balanced coalgebroids,” Theory and Applications of Categories, vol. 7, no. 6, pp. 71–147, 2000.

[69] J. Hefford and C. Comfort, “Coend Optics for Quantum Combs,” in Proceedings ACT 2022, vol. 380, 2023, pp. 63–76.

## APPENDIX A
PROOFS

### A. Distributor in Chu($C$, $\perp$)

The following diagram commutes.

<figure><img src="image_22.png" /></figure>

Here $\text{ten}_\otimes$ is the canonical map that comes from currying the duoidal distributor and the evaluation morphisms,

$$([a, b] \otimes [c, d]) \otimes (a \otimes c) \xrightarrow{\delta} ([a, b] \otimes a) \otimes ([c, d] \otimes c) \xrightarrow{\text{ev} \otimes \text{ev}} b \otimes d$$

The unlabelled arrows are the canonical ones arising in the pullbacks we are working with. The desired arrow

$$ \begin{aligned} [a, c'] \times_{[a \otimes c, \perp]} [c, a'] \otimes & ([b, d'] \times_{[b \otimes d, \perp]} [d, b']) \\ & \to [ab, c'd'] \times_{[ab \otimes cd, \perp]} [cd, a'b'] \end{aligned} $$

arises from the universal property of the pullback.

### B. Proof of Theorem 1

*Proof:* Suppose $F$ is a $*$-functor. Since $F$ is $\otimes$-lax, $(F, F(-)^*) := \bar{F}(-)$) is a linear functor by the results of [48]. The natural isomorphism $s : (Fa)^* \to Fa^*$ induces a natural isomorphism $k$ between $F$ and its de Morgan dual $\bar{F}$.

<figure><img src="image_23.png" /></figure>

So $F$ becomes $\mathfrak{N}$-colax with colaxator $l_\mathfrak{N}$ inherited from that of $\bar{F}$. $(F, F)$ then becomes a degenerate linear functor so long as we can lift the linear coherences of $(F, \bar{F})$ along the isomorphism $k$.

In particular we want the outside of following diagram to commute, which it does if the three squares containing exclamation marks commute.

<figure><img src="image_24.png" /></figure>

So we require the following square to commute relating the laxator $l_\otimes$ and the linear strength $\bar{l}_\otimes$,

$$ \begin{array}{ccc} F(a) \otimes F(b) & \xrightarrow{1 \otimes k_b} & Fa \otimes (Fb^*)^* \\ \multicolumn{1}{c}{l_\otimes} & \multicolumn{1}{c}{\downarrow} & \multicolumn{1}{c}{\bar{l}_\otimes} \\ F(a \otimes b) & \xrightarrow{k_a \otimes b} & (F(a \otimes b)^*)^* \end{array} \qquad (14) $$

and the following triangle relating the colaxator $l_\mathfrak{N}$ to the strength $\bar{l}_\mathfrak{N}$.

$$ \begin{array}{ccc} F(a \mathfrak{N} b) & \xrightarrow{\bar{l}_\mathfrak{N}} & \bar{F}a \mathfrak{N} Fb \\ \multicolumn{1}{c}{l_\mathfrak{N}} & \multicolumn{1}{c}{\downarrow} & \multicolumn{1}{c}{k_a \mathfrak{N} 1} \\ \bar{F}a \mathfrak{N} Fb & & \end{array} \qquad (15) $$

Let us start by proving that (14) commutes. The coherence (4) for the $*$-functor $F$ has the following presentation in the string diagrams (proof nets),

<figure><img src="image_25.png" /></figure>
where the black dot is given by

<figure><img src="image_26.png" /></figure>

Square (14) takes the following form where the diagram for the linear strength $\bar{l}_{\otimes}$ can be found in [48].

<figure><img src="image_27.png" /></figure>

Which can be seen to hold by the following graphical manipulations.

<figure><img src="image_28.png" /></figure>

The triangle (15) takes the following form (again, see [48] for the diagrams for the linear costrength and the colaxator).

<figure><img src="image_29.png" /></figure>

That this holds follows very similarly to the case of the laxator and linear strength.

<figure><img src="image_30.png" /></figure>

So we have shown that the coherence (4) is sufficient to ensure that the laxator coincides with the linear strength and the colaxator with the linear costrength (up to the induced isomorphism $k$). As a result $(F, F)$ becomes a linear functor.
Now we show the converse. So suppose that $(F, F)$ is a linear functor. Then $(F, \bar{F})$ is also linear and linearly equivalent to $(F, F)$, so that (14) and (15) commute. Upon taking $b$ to be $i_\otimes$ in (14) and composing by the laxator $l_0$ and the map $F\rho^*$ one recovers the coherence (4). The left hand side of (14) becomes the following.

<figure><img src="image_31.png" /></figure>

While the right hand side of (14) becomes the following.

<figure><img src="image_32.png" /></figure>

<figure><img src="image_33.png" /></figure>

<figure><img src="image_34.png" /></figure>

Let us now comment on a few other notable coherence issues. Firstly, one might be concerned that there are two canonical natural isomorphisms $Fa \cong \bar{Fa}$, one given by $\bar{Fa} \xrightarrow{s_a^*} (Fa)^{**} \xrightarrow{d_{Fa}} Fa$ and the other given by $\bar{Fa} \xrightarrow{s_{a^*}} Fa^{**} \xrightarrow{Fd} Fa$ where $d : a^{**} \to a$ is the double dualisation natural isomorphism. In fact, these two natural isomorphisms agree for any $*-functor.

**Lemma 3:** Let $F$ be a $*-functor$, then the following diagram commutes.

<figure><img src="image_35.png" /></figure>

Proof:

<figure><img src="image_36.png" /></figure>

Bending up the right-hand input completes the proof.

<figure><img src="image_37.png" /></figure>

<figure><img src="image_38.png" /></figure>

### C. Proof of Proposition 1

*Proof:* There is an isomorphism $\mathrm{Chu}(\mathcal{C}, \perp_{\mathcal{C}}) \times \mathrm{Chu}(\mathcal{D}, \perp_{\mathcal{D}}) \cong \mathrm{Chu}(\mathcal{C} \times \mathcal{D}, (\perp_{\mathcal{C}}, \perp_{\mathcal{D}}))$. The $*-functor$ witnessing this acts on objects in the intuitive fashion,

$$ ((c, c', r), (d, d', s)) \mapsto ((c, d), (c', d'), (r, s)) $$

and on morphisms as

$$ ((f, f'), (g, g')) \mapsto ((f, g), (f'g')). $$
Functoriality and *-commutation are immediate. Writing 1 for the terminal CSMC, with one object •, it is clear that Chu(1, •) has only one object and is isomorphic to the terminal *-autonomous category. The required 2-cells (see e.g. [67]) are straightforward to define and are all isomorphisms. ■

### D. Proof of Theorem 2

*Proof:* A pseudomonoid in *Aut is a *-autonomous category $\mathcal{C}$ equipped two *-functors $\otimes - \otimes : \mathcal{C} \times \mathcal{C} \to \mathcal{C}$ and $i_{\otimes}: 1 \to \mathcal{C}$ and natural isomorphisms making these essentially associative and unital. Since *-functors are equivalent to degenerate linear functors between *-autonomous categories by Theorem 1, we see that we recover the definition of a pre-BV-category given in [39].

The normality of functors in $\mathrm{Aut}_N$ enforces the extra condition $i_{\otimes} \cong i_{\otimes}$ making a pseudomonoid here a BV-category. ■

### E. Proof of Theorem 3

*Proof:* By Proposition 1, Chu is a strong monoidal 2-functor. Any (even lax) monoidal 2-functor $F: \mathcal{C} \to \mathcal{D}$ preserves pseudomonoids [67], and furthermore lifts along the forgetful functors $U$ to a 2-functor $F: \mathrm{PsMon}(\mathcal{C}) \to \mathrm{PsMon}(\mathcal{D})$ such that the following diagram commutes [68].

<figure><img src="image_39.png" /></figure>

From now on we identify Chu with $\mathrm{PsMon}(\mathrm{Chu})$ whenever the context is clear. So, if $(\mathcal{C}, \perp)$ is a pseudomonoid in $\mathrm{CSMC}_{\perp}$ then $\mathrm{Chu}(\mathcal{C}, \perp)$ is automatically a pseudomonoid in $\mathrm{Aut}$, that is, a pre-BV-category by Theorem 2.

Now consider a pseudomonoid in $\mathrm{CSMC}_{\perp}$. This consists of a multiplication and unit of the form,

$$ \otimes : (\mathcal{C}, \perp) \times (\mathcal{C}, \perp) \to (\mathcal{C}, \perp), \quad i_{\otimes} : (1, \bullet) \to (\mathcal{C}, \perp). $$

This makes $\mathcal{C}$ a $\otimes$-closed, $\otimes$-symmetric duoidal category with all pullbacks. Since $\otimes$ must laxly preserve the chosen objects, we have morphisms $\perp \otimes \perp \to \perp$ and $i_{\otimes} \to \perp$ making $\perp$ a $\otimes$-monoid; the associativity and unitality come from those of the pseudomonoid. ■

### F. Proof of Theorem 4

*Proof:* The proof proceeds much like the previous one. By Proposition 1, Chu is strongly monoidal and therefore sends pseudomonoids to pseudomonoids. So, if $(\mathcal{C}, \perp)$ is a pseudomonoid in $\mathrm{CSMC}_{\mathbb{N}, \perp}$ then $\mathrm{Chu}(\mathcal{C}, \perp)$ is a pseudomonoid in $\mathrm{Aut}_N$, that is, a BV-category.

Now consider a pseudomonoid on $(\mathcal{C}, \perp)$ in $\mathrm{CSMC}_{\mathbb{N}, \perp}$. This makes $\mathcal{C}$ a $\otimes$-closed, $\otimes$-symmetric normal duoidal category with all pullbacks. Now $\otimes$ must preserve the chosen objects, giving isomorphisms $\perp \otimes \perp \cong \perp$ and $i_{\otimes} \cong \perp$. The latter, along with normality of the duoidal structure implying that $\perp \cong i_{\otimes}$. ■

### G. Proof of Theorem 6

*Proof:* As outlined in the main text, morphisms of type $\otimes_i(C_{a_i}, y_{a_i}) \to \mathfrak{N}_k(C_{a_k}, y_{a_k})$ are strong natural transformations of the form $\otimes_i C_{a_i} \to C_b$ with $b := (\otimes_k b_k, \otimes_k b'_k)$ such that when all but one of their inputs are filled they return an optic.

On the other hand, it is known that all unitary supermaps decompose locally as a comb [57]. As a result, it was proven in [21] that there is a polycategory $\mathrm{srep}(\mathcal{C})$ equivalent to uQS whose polymorphisms are taken to be strong natural transformations $S: \otimes_i C_{a_i} \to C_b$ with $b := (\otimes_k b_k, \otimes_k b'_k)$ such that when evaluated on all but one input they return a comb.

All that remains is to use the equivalence between unitary optics and unitary quantum combs proven in [69]. ■