Categorifying the ZX-calculus
Daniel Cicala (University of California, Riverside)

TL;DR
This paper develops a bicategorical framework combining spans and cospans within a topos to study open networks and diagrammatic languages, exemplified by the ZX-calculus.
Contribution
It introduces a new bicategory construction that integrates the ZX-calculus, providing a formal categorical setting for diagrammatic reasoning.
Findings
Constructed a symmetric monoidal, compact closed bicategory
Applied the framework to the ZX-calculus diagrams
Provided a categorical foundation for diagrammatic languages
Abstract
We build a symmetric monoidal and compact closed bicategory by combining spans and cospans inside a topos. This can be used as a framework in which to study open networks and diagrammatic languages. We illustrate this framework with Coecke and Duncan's zx-calculus by constructing a bicategory with the natural numbers for 0-cells, the zx-calculus diagrams for 1-cells, and rewrite rules for 2-cells.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Categorifying the ZX-calculus
Daniel Cicala University of California, RiversideDepartment of Mathematics [email protected]
Abstract
We build a symmetric monoidal and compact closed bicategory by combining spans and cospans inside a topos. This can be used as a framework in which to study open networks and diagrammatic languages. We illustrate this framework with Coecke and Duncan’s zx-calculus by constructing a bicategory with the natural numbers for 0-cells, the zx-calculus diagrams for 1-cells, and rewrite rules for 2-cells.
1 Introduction
Compositionality is increasingly becoming recognized as a viable point of view from which to study complex systems such as those found in physics [2], computer science [38], and biology [7]. The focus is on connecting together smaller, simpler systems. The word ‘compositionality’ suggests the relevancy of category theory. This is indeed the case. In fact, this paper fits into a larger project of establishing suitable categorical frameworks in which to study composable systems [5, 6, 7, 26, 9, 10, 36]. Open diagrams and diagrammatic languages are typical players in compositional approaches. In our context, the adjective ‘open’ is an established term [30, 32, 36] referring to a structure equipped with chosen inputs and outputs. The primary advantage of open diagrams is the ability to work within a more intuitive syntax. Such diagrams are typically constructed with graph or topological string-like objects. Occasionally, additional data is attached to nodes, edges, or strings as needed. For example, open Markov chains [36] use graphs whose nodes are labeled with a population and edges with the rate at which the population of the source node shifts to the target node.
Another common feature shared between diagrammatic languages is the notion of equality. Formal languages are often equipped with a collection of rewrite rules. For us, a rewrite rule is an equivalence relation on diagrams stating when we can replace a diagram with diagram . This is our equality.
Currently, syntax for diagrammatic calculi are usually captured with 1-categories by encoding diagrams as morphisms and diagram connection by composition. As mentioned above, rewrite rules provide a notion of equality between diagrams. However, 1-categorical frameworks squash the information contained in a rewrite rule. That is, there is no way to reconstruct a rewrite rule from an equality. To more fully capture a system, rewrite rules ought to have better representation in our syntax. We accomplish this is by including them as 2-cells in a bicategory.
What should such a bicategory look like? The 0-cells should communicate whether a pair of diagrams can be connected. Taking 0-cells to be sets, then a 1-cell is a diagram whose set of inputs is and set of outputs is . Hence, we can connect to any diagram whose inputs are or outputs are . The 2-cells are rules that rewrite into .
To better envision such a bicategory, consider a hypothetical system modeled by a directed graph . Suppose that we would like to have inputs and outputs , each subsets of the -nodes. We can build this information into a cospan of graphs by taking and to be edgeless graphs. Our 1-cells are cospans like this. This means that the inputs and outputs are [math]-cells. Rewrite rules are included through double pushout rewriting [18]. This presents a rule rewriting to as a span of graphs , through some intermediary graph . As 2-cells in our bicategory, rewrite rules are isomorphism classes of spans of cospans. These are depicted in Figure 2. Kissinger [28] also modeled rewriting using spans of cospans under the term cospan rewrites.
The author proved that this construction actually gives a bicategory [9]. In particular, starting with a topos , there is a bicategory whose 0-cells are the -objects, 1-cells are cospans in , and 2-cells are isomorphism classes of monic legged spans of cospans in . A topos and monic span legs are required to ensure that the interchange law holds. This is not overly restrictive, because the spans used in double pushout rewriting are often assumed to have monic legs [25]. Though not discussed in that paper, we can bypass both needs by taking coarser classes of 2-cells. Specifically, we consider the bicategory where is a category with finite limits and colimits. This differs from by taking 2-cells to be all spans of cospans up to having the same domain and codomain.
The reason for constructing and is to provide syntactic bicategories for diagrammatic languages. Which bicategory we use depends on the nature of the diagrammatic language of interest. Regardless of which bicategory we use, we typically start by letting or be the topos of directed graphs or, perhaps, the topos consisting of some other flavor of graphs. For now, we look at and and consider, in each, the sub-bicategory that is 1-full and 2-full on the edgeless graphs. The 1-cells this sub-bicategory are open graphs and the 2-cells are ways to rewrite one open graph to another. Because we are currently painting with broad strokes, distinguishing between this sub-bicategory in or is inconsequential. Hence, we commit the sin of referring to this bicategory as regardless of where it lives.
Suppose we have a diagrammatic language given by some presentation. We must find a suitable way to identity the given generators and relations of with 1-cells and 2-cells, respectively, of . These 1-cells and 2-cells, in turn, generate a sub-bicategory of that gives a bicategorical syntax for . It was shown by the author and Courser [10] that is symmetric monoidal and compact closed in the sense of Stay [41]. We employ a similar argument showing the same is true of . Therefore and all of sub-bicategories we generate within are symmetric monoidal and compact closed.
Due to using isomorphism classes for 2-cells instead of any other equivalence classes, it would seem that beginning with is the natural construction. Indeed, it is suitable for working with systems admitting a graphical syntax such as the open Markov processes mentioned above. However, systems whose syntax has topological information, like string diagrams, introduce the challenge of conveying topological information with only graphs. To contend with this problem, we begin with because it has a 2-cell not present in . This 2-cell rewrites an edge into a single node, thus forces an analogy between an edge and a string that behaves like an identity. As we will see, this rewrite rule is given by a span with a non-monomorphic leg, leading us to use instead of .
The purpose of this paper is to illustrate our framework with the zx-calculus. The backstory of the zx-calculus dates to Penrose’s tensor networks [35] and, more recently, to the relationship between graphical languages and monoidal categories [27, 39]. Abramsky and Coecke capitalized on this relationship when inventing a categorical framework for quantum physics [2]. Soon after, Coecke and Duncan introduced a diagrammatic language in which to reason about complementary quantum observables [11]. After a fruitful period of development [14, 17, 21, 22, 23, 34], a full presentation of the zx-calculus was published [12]. The completeness of the zx-calculus for stabilizer quantum mechanics was later shown by Backens [4].
The zx-calculus begins with the five diagrams depicted in Figure 1.
The dangling wires on the diagrams’ left are inputs and those on the right are outputs. By connecting inputs to outputs, we can form larger diagrams. Formalizing this perspective, we let these diagrams generate the morphisms of a dagger compact category whose objects, the non-negative integers, count the inputs and outputs of a diagram. Section 2 contains a presentation of along with a brief discussion on the origins of the generating morphisms (Figure 1) and relations (Figure 3). We also mention relevant software, Quantomatic [2, 29] and Globular [8].
Our goal in this paper is to generate a symmetric monoidal and compact closed (SMCC) bicategory that provides a syntax for the zx-calculus. Our first steps towards constructing is in Section 3 where we fit open graphs into an SMCC bicategory. To this end, we slightly modify recent work by Courser and the author [9, 10] in order to produce an SMCC bicategory with graphs as 0-cells, cospans of graphs as 1-cells, and certain equivalence classes of spans of cospans of graphs as 2-cells (see Figure 2). As discussed above, this has an SMCC sub-bicategory that provides an ambient space in which to generate systems modeled on open graphs.
However, this version of does not contain everything we need. In Section 4, we fill the gap by introducing open graphs over . That is, we pick a graph
[TABLE]
whose nodes coincide with the node types found in the zx-calculus diagrams, with one exception: the white node in the center. This node replaces the dangling edges in the zx-diagrams. A graph morphism then corresponds to a zx-morphism by transporting the node types to via the fibres of the map. In his thesis [28], Kissinger also colored graphs this way. We then form an SMCC bicategory with graphs over as 0-cells, cospans of graphs over as 1-cells, and spans of cospans as 2-cells. These spans of cospans are taken up to the equivalence relation obtained by relating 2-cells with the same domain and codomain. In analogy to the formation of , we find a sub-bicategory that can be thought of as containing all open graphs over and their rewrites.
The bicategory is a space in which we can generate SMCC sub-bicategories. In Section 5, we give a presentation for a sub-bicategory of whose 1-cells correspond to zx-calculus diagrams and 2-cells to the relations between them. After constructing , we decategorify it to a 1-category by identifying 1-cells whenever there is a 2-cell between them. Though this seems asymmetrical, we actually get an equivalence relation because of the dual nature of spans. In the main result, Theorem 5.4, we construct a dagger compact functor witnessing an equivalence of categories. It is in this sense that we are categorifying the zx-calculus.
The author would like to thank John Baez for many helpful ideas and discussions that contributed to this paper. A debt of gratitude is also owed to three anonymous referees for their insightful comments on an earlier version of this paper written for the 2017 Quantum Physics and Logic conference in Nijmegen, Netherlands.
2 The zx-calculus
One of the most fascinating features of quantum physics is the incompatibility of observables. Roughly, an observable is a measurable quantity of some system, for instance the spin of a photon. Incompatibility is in stark contrast to classical physics where measurable quantities are compatible in that, we can obtain arbitrarily precise values at the same time. Arguably, the most famous example of incompatibility is Heisenberg’s uncertainty principal which places limits to the precision that one can simultaneously measure a pair of observables: position and momentum. There are different levels of incompatibility amongst pairs of observables. When such a pair is maximally incompatible, meaning that knowing one with complete precision implies total uncertainty of the other, we say they are complementary observables.
Hilbert spaces are, historically, the typical framework in which one might study observables. This formalism has been quite successful despite involving difficult calculations and non-intuitive notation.
The zx-calculus was developed by Coecke and Duncan [12] as a high-level language to facilitate such computation between complementary observables. It was immediately used to generalize both quantum circuits [33] and the measurement calculus [19]. Its validity was further justified when Duncan and Perdrix presented a non-trivial method of verifying measurement-based quantum computations [22]. At its core, the zx-calculus is an intuitive graphical language in which to reason about complementary observables.
The five basic diagrams in the zx-calculus are depicted in Figure 1 and are to be read from left to right. They are
- •
a wire with a single input and output,
- •
green spiders with a non-negative integer number of inputs and outputs and paired with a phase ,
- •
red spiders with a non-negative integer number inputs and outputs and paired with a phase ,
- •
the Hadamard node with a single input and output, and
- •
a diamond node with no inputs or outputs.
The wire plays the role of an identity, much like a plain wire in an electrical circuit, or straight pipe in a plumbing system. The green and red spiders arise from a pair of complementary observables. Incredibly, observables correspond to certain commutative Frobenius algebras living in a dagger symmetric monoidal category . Moreover, a pair of complementary observables gives a pair of Frobenius algebras whose operations interact via laws like those of a Hopf algebra [15, 16]. This is particularly nice because Frobenius algebras have beautiful string diagram representations. If is the monoidal unit of , there is an isomorphism of commutative monoids that gives rise to a group structure on known as the phase group. The spider phases arise from this group. The Hadamard node embodies the Hadamard gate. The diamond is a scalar obtained when connecting a green and red node together. A deeper exploration of these notions goes beyond the scope of this paper. For those interested, the original paper on the topic [12] is an excellent place read more.
In the spirit of compositionality, we present a category below whose morphisms are generated by the five basic diagrams. To anticipate the shift in terminology, we will refer to zx-calculus diagrams as -morphisms and continue to use the qualifier ‘basic’ in the same way.
Observe that there is a non-negative number of wires dangling on the left and right side of each basic -morphism. Those on the left, we call inputs and those on the right outputs. These basic -morphisms generate the morphisms of a dagger compact category whose objects are the non-negative integers. This category was introduced by Coecke and Duncan [12] and further studied by Backens [4]. To compose in , connect compatible diagrams along an enumeration of the the inputs and the outputs. A monoidal structure is given by adding numbers and taking the disjoint union of -morphisms. Relations between the morphisms are given below, but we note here that the wire is the identity on . The identity on is the disjoint union of wires. The symmetry and compactness of the monoidal product provide a braiding, evaluation, and coevaluation morphisms: respectively,
[TABLE]
The evaluation and coevalutation maps are of type and for each object and the empty diagram for . On the spider diagrams, the dagger structure swapps inputs and outputs then, multiplies the phase by :
[TABLE]
The dagger acts trivially on the wire, Hadamard, and diamond elements.
Thus far, we have a presentation for a free dagger compact category. However, there are relations between -morphisms. These are given in Figure 3, though we also include equations obtained by exchanging red and green nodes, daggering, and taking diagrams up to ambient isotopy in -space. These listed relations are called basic. Spiders with no phase indicated have a phase of [math]. The emergence of these relations goes beyond the scope of this paper and we point the interested reader to the genesis of the zx-calculus [12] for an explanation.
A major advantage of using string diagrams, apart from their intuitive nature, is that computations are more easily programmed into computers. Indeed, graphical proof assistants like Quantomatic [8, 20] and Globular [8] were tailor made for such graphical reasoning. The logic of these programs are encapsulated by double pushout rewrite rules. However, the algebraic structure of and other graphical calculi do not contain the rewrite rules as explicit elements. Perhaps, conceiving of rewrite rules as actual elements in the syntax can prove beneficial for software programmers.
3 Rewriting open graphs
Surely, the -morphisms are reminiscent of directed graphs. Hence there is a reasonable optimism that we can model the zx-calculus with graphs. However, our hope is tempered by some clear differences between graphs and -morphisms. For one, graphs do not have inputs or outputs. In this section, we reconcile this particular difference by using open graphs.
Open graphs and their morphisms have been considered by Dixon, Duncan, and Kissinger [30] though our conceit is slightly different. Conceptually, open graphs are quite simple. Take a directed graph and declare some of the nodes to be inputs and others to be outputs, for example
[TABLE]
Given open graphs and , if the set of inputs in and the set of outputs in have the same cardinality, we can glue them together along a bijection. This gives a way to turn a pair of compatible open graphs into a single open graph. For instance, to the above open graph, we can connect
[TABLE]
to form
[TABLE]
We make this precise with cospans and pushouts.
Definition 3.1**.**
Consider the functor , on a skeleton of , defined by the letting be the edgeless graph with nodes . An open graph is then a cospan in the category of the form for sets and .
The left leg of the cospan gives the input and the right leg the outputs. Suppose we have another open graph with inputs and outputs . Then we can compose cospans
[TABLE]
by pushing out over to get
[TABLE]
By taking isomorphism classes of these pushouts, we obtain a category whose objects are those in the image of and morphisms are open graphs. But we can do better!
Thus far, we have only just described the first layer of bicategory introduced by the author under the name [9]. It was shown in a joint work with Courser [10] that is symmetric monoidal and compact closed. The monoidal structure is induced from the coproduct of graphs. Here, we take Stay’s definition of compact closedness for bicategories [41]. As discussed in the introduction, we will work instead with the slightly modified version of described in Definition 3.3.
Construction on this modified bicategory begins with the theorem below. First, we introduce some needed terminology. A span of cospans is a commuting diagram as illustrated in Figure 2. A parallel class of spans of cospans is formed by the equivalence relation given by identifying spans of cospans with same domain and codomain.
Theorem 3.2**.**
Let be a finitely complete and cocomplete (braided, symmetric) monoidal category such that preserves colimits. There is a (braided, symmetric) monoidal bicategory whose 0-cells are -objects, 1-cells are cospans in , and 2-cells are parallel classes of spans of cospans. In case is cocartesian, then is also compact closed.
We prove this theorem in Appendix A. It follows from taking parallel classes of 2-cells that hom-categories in are groupoids.
Using parallel classes of 2-cells instead of isomorphism classes has several advantages. First, it removes two conditions required of in : that be a topos and that the legs in the span of cospans be monic. It also allows us, when is sufficiently like , to rewrite an edge into a node in analogy to deforming a topological string into a point. Moreover, these 2-cells give us unitary 1-cells.
Recall there are two ways to compose 2-cells in a bicategory. Horizontal composition in uses pushouts and vertical composition uses pullbacks:
[TABLE]
Definition 3.3**.**
Define to be the 1-full and 2-full SMCC sub-bicategory of whose 0-cells are exactly those graphs in the image of the functor .
The conceit of is that the 1-cells are open graphs whose inputs and outputs are chosen by the [math]-cells, and the -cells are rewrite rules that preserves the input and output nodes. By rewrite rules, we mean those taken from the double pushout graph rewriting approach [18]. Our open graphs are a different formulation of what amounts to the same concept explored by Dixon, Duncan, and Kissinger [30] though we go a bit further, getting an SMCC bicategory of open graphs instead of a 1-category.
Our motivation for constructing is not to study it directly, but for it to serve as an ambient context in which to generate SMCC sub-bicategories on some collection of open graphs and rewriting rules. Presenting categories by open graphs and rewrite rules is common enough [30, 24, 36] to warrant finding a common framework in which to fit such categories. However, there are drawbacks to this approach. For example, working with open graphs is only useful to model graphical languages whose terms are equal up to ambient isotopy in -space. This limits the current approach to only symmetric monoidal (bi)categories as Selinger’s work shows [39].
Employing open graphs is not quite enough for us to fully capture the zx-calculus. We still need to color our open graphs in a way that corresponds to the zx-diagram node types.
4 Open graphs over
Last section, we began the process of modeling the zx-calculus with graphs by introducing open graphs and fitting them into a bicategory . This overcame the issue of graphs lacking inputs and outputs. In this section, we face a different issue. Unlike open graphs, -morphisms have multi-sorted nodes. In this section, we equip open graphs with multi-sorted nodes by working with a slice category of . Kissinger used a similar method to give graphs multi-sorted nodes in his thesis [28].
Definition 4.1**.**
Let be a graph. By a graph over , we mean a graph morphism . A morphism between graphs over is a graph morphism such that the following diagram commutes
[TABLE]
Every graph morphism contains a map between corresponding nodes sets. The fibre of this map colors the -nodes with the -nodes. We illustrate this with the following example.
Example 4.2**.**
Let be the graph
[TABLE]
We have not drawn the entirety of . The green and red nodes actually run through and all of them have a single arrow to and from node .
Most of the structure of the basic -morphisms is captured by graphs over . Consider the following graphs over
[TABLE]
[TABLE]
where the diagrams give the domain of each graph over and the map is described directly underneath each diagram. The behavior of each map is determined by the image of the nodes because there is at most one arrow between any two nodes in . The role played by each node of in providing our desired structure is evident except, perhaps, for the node . Observe that four of the basic -morphisms have dangling wires on either end. Because edges of directed graphs must be attached to a pair of nodes, we use this node to anchor the dangling edges.
Example 4.3**.**
At this point, we can interpret the basic zx-diagrams as graphs over . This extends nicely to a translation of any -morphism, such as
[TABLE]
which corresponds to the -morphism
[TABLE]
The graphs over in Examples 4.2 and 4.3 capture most of the structure of the basic -morphisms. The ability to compose is still missing. Composition becomes possible with open graphs over . Again, we use cospans to make this precise, though combining these two structure introduces new considerations.
Start with the slice category of graphs over . By Theorem 3.2, this gives us an SMCC bicategory within which we want to construct a sub-bicategory analogous to . However, there is a problem. Recall that the objects of have form where is the functor sending a set to the edgeless graph on that set. In , there is a unique, up to isomorphism, way to be an edgeless graph. But in , there may be many ways to be edgeless. This depends on the number of graph morphisms to . For instance, a graph with nodes and no edges can be a graph over in ways. We rectify this issue by functorially turning a set into an edgeless graph. Recall that is a skeleton of .
Definition 4.4**.**
Define a functor by
[TABLE]
where is the edgeless graph with nodes that are constant over . An open graph over is a cospan in of the form
[TABLE]
With this definition of open graphs over , we propose the analogue to .
Definition 4.5**.**
Define to be the symmetric monoidal and compact closed sub-bicategory of that is 1-full and 2-full on objects of the form for finite sets .
Unpacking this definition, the 0-cells of are those edgeless graphs over in the image of . The 1-cells are exactly the open graphs over . The 2-cells are the rewritings of one open graph over into that preserve the inputs and outputs. To better understand this bicategory, we give an example of an open graph over . Along with this example, we present a new notation that allow us to draw the remaining diagrams more compactly.
Example 4.6**.**
Consider the graph over in Example 4.3. Make this an open graph as follows:
[TABLE]
There is a single input, node , and a single output, node . Denote this by
[TABLE]
The input nodes are aligned on the far left and the output nodes on the far right. The ’s in the corners refer to the cardinality of the input and output node sets. This may seem unnecessary or redundant, but it will clarify several situations arising later on. Thus, we side with consistency and always write the cardinalities. Of course, this notation strips a fair amount information regarding the graph morphisms involved in the cospan. However, any missing information should be evident in context.
Recall that our interest in is as an ambient space in which to generate syntactical bicategories for graphical languages. The same is true of our new bicategory . Presently, we are interested in 1-cells corresponding to the basic -morphisms and 2-cells to the basic relations depicted in Figure 3. We claim that the bicategory generated by these 1-cells and 2-cells categorifies .
5 A categorification of
Section 4 describes a translation of the basic -morphisms into open graphs over . These are depicted in Figure 4 and are referred to as basic open graphs over . To clarify the double instances of and written in the spider diagrams, those below the diagram refer to the cardinalities of the cospan legs, and those beside the brackets count how many nodes are there (cf. Example 4.6).
Just as the basic open graphs over capture the generating -morphisms, we must also include the basic relations into our framework. Figure 5 depicts our representation of the basic relations as spans of open graphs. In addition to the basic relations listed explicitly, we add those obtained by exchanging red and green nodes, swapping inputs and outputs, turning the spans around, as well as
[TABLE]
The last is added to ensure that the wire 1-cell behaves as the identity, a property we lose when using graphs. All of these 2-cells, we call basic.
It is important to emphasize that the basic 2-cells are representatives of an equivalence class. That is, we have made a decision to present these 2-cells as a span of cospans whose apex is the edgeless graph whose node set is the disjoint union of the inputs and outputs. This is certainly not the only representative we could have chosen, though it does seem to be the most natural choice.
Forget for a moment that our 2-cells are classes and think of only the representatives. When we compose a span of cospans with its dagger, we get a non-trivial way to rewrite a 1-cell into itself. This ought to be distinct from the identity rewrite, which does nothing. However, our choice of equivalence classes render these the same. This hints that a higher rewriting structure is hiding in the background. Indeed, conveying rewrite rules as spans of cospans has the advantage of including higher level rewrite rules in by iterating the process of taking spans. Currently, we content ourselves to work within bicategories and leave an exploration for higher structure for another time.
We now define the bicategory which categorifies the zx-calculus.
Definition 5.1**.**
Define to be the symmetric monoidal and compact closed sub-bicategory of generated by the basic -cells and basic -cells.
Working within allows us to generate as an SMCC in this way. Without having this ambient space, we cannot be sure that we obtain an SMCC bicategory simply by giving a presentation.
Because is symmetric monoidal and compact closed, it contains twist, evaluation, and coevaluation 1-cells
[TABLE]
witnessing symmetry and the compact structure on .
Horizontal and vertical composition are the same as in 1. For example, we can compose spider diagrams with the same number of inputs and outputs:
[TABLE]
We tensor 1-cells by disjoint union, such as
[TABLE]
With defined, we turn our focus towards presenting the main theorem. We start by giving a category that is a decategorification or truncation of .
Definition 5.2**.**
Define to be the category whose objects are the 0-cells of and whose arrows are the 1-cells of modulo the equivalence relation given by: if and only if there is a 2-cell in .
To be clear, is an equivalence relation and doesn’t merely generate one. This follows from the symmetry of spans and vertical composition.
Theorem 5.3**.**
The category is dagger compact via the identity-on-objects functor given by
[TABLE]
as well as by identity on the wire, Hadamard, and diamond morphisms.
Proof.
Compact closedness follows from the self duality of objects via the evaluation and coevaluation maps from (4). The snake equation is derived by
[TABLE]
where the equalities follow from the evident 2-cells in . The extra relation (3) ensures that the string of wires is the identity. Showing that is a dagger functor is a matter of checking some easily verified details. ∎
Theorem 5.4**.**
The identity on objects, dagger compact functor given by
[TABLE]
[TABLE]
is an equivalence of categories.
Proof.
That is identity-on-objects implies essential surjectivity. Fullness holds because the generating morphisms for are all in the image of .
Proving faithfulness is more involved. Let and be -morphisms. Consider representatives , of , obtained by translating directly the graphical representation of to open graphs over as in Examples 4.3 and 4.6. It suffices to show that the existence of a 2-cell in implies that .
Observe that any 2-cell in can be written, not necessarily uniquely, as a sequence where each is a basic 2-cell, each box is filled with ‘’, ‘’, or ‘’, and parentheses are right justified. By ‘’ and ‘’, we mean horizontal and vertical composition. We induct on sequence length. If is a basic 2-cell, then there is clearly a corresponding basic relation equating and . Suppose we have a sequence of length such that the left-most square is a ‘’. Then we have a 2-cell where is a basic 2-cell and can be written with length . By fullness, we can write where . This gives that and the result follows. A similar argument handles the cases when the left-most operation is vertical or horizontal composition. ∎
6 Conclusion
The main advantage of fitting the zx-calculus into a bicategory is that the rewrite rules are now explicitly included into the mathematical structure. That is, we are now capturing a larger portion of the full picture that is the zx-calculus.
However, categorifying the zx-calculus is only part of the story. The methods used here are general with only slight tweaks made to accommodate the case at hand. Indeed, similarly to how we use to capture zx-diagrams, we can construct modified versions of to frame open Markov chains, resistor networks, internal Frobenius algebras, etc into this framework.
Appendix A A symmetric monoidal bicategory of spans of cospans
In this section, we prove Theorem 3.2. Let be a finitely complete and cocomplete (braided, symmetric) monoidal category such that preserves colimits. The category together with its coproduct is one example. The proof consists of two parts: that is a (braided, symmetric) monoidal bicategory and that it is compact closed.
We first show is a (braided, symmetric) monoidal bicategory with a result from Shulman.
Theorem A.1**.**
[40*, Theorem 5.1]**
Let be an isofibrant (braided, symmetric) monoidal double category. There is a (braided, symmetric) monoidal bicategory whose objects are those of and whose hom-categories have as objects the horizontal arrows in of type and as morphisms the 2-cells in of type*
[TABLE]
The same paper [40] also contains the definitions used in this section. To use this theorem, we begin construction on a double category . This requires cubical spans of cospans, which are commuting diagrams of shape
[TABLE]
We get an equivalence relation on these by relating cubical spans of cospans that share the same outside square. The induced classes are called parallel classes.
Lemma A.2**.**
There is a double category whose objects are the -objects, vertical morphisms are given by isomorphism classes of spans in with invertible legs, horizontal morphisms are given by cospans in , and 2-morphisms are parallel classes of cubical spans of cospans in .
Proof.
Define the object category to have as objects the -objects and as morphisms the isomorphism classes of spans in with invertible legs. Define the arrow category to have as objects the cospans in and as morphisms the parallel classes of cubical spans of cospans in .
The structure functor acts on objects by mapping to the identity cospan on and on morphisms by mapping , whose legs are isomorphisms, to
[TABLE]
The source functor acts on objects by sending to and on morphisms by sending a cubical span of cospans to the span occupying the left vertical side. The target functor is defined similarly.
The horizontal composition functor acts on objects by composing cospans with pushouts in the usual way. It acts on morphisms by
[TABLE]
This respects identities and we separate the proof that respects composition into the next lemma. It is straightforward to check that the required equations are satisfied. The associators and unitors arise from universal properties. ∎
Lemma A.3**.**
The assignment from Lemma A.2 preserves composition. In particular, is a functor.
Proof.
Let be the following 2-morphisms
[TABLE]
[TABLE]
Our goal is to show that
[TABLE]
The left hand side of this equation corresponds to horizontal composition before vertical composition. The right hand side corresponds to composing in the opposite order.
First, compute the left hand side of (5). Composing horizontally, and are, respectively,
[TABLE]
The vertical composite is equal to
[TABLE]
Now solving for the right hand side of (5), and are respectively
[TABLE]
The vertical composite is equal to
[TABLE]
Since (6) and (7) have coinciding outer squares, they represent the same parallel class, hence (5) holds. ∎
Our next step is to show that the (braided, symmetric) monoidal structure from lifts to . We point to [40, Def. 2.9] for the definition of a monoidal double category.
Lemma A.4**.**
The (braided, symmetric) monoidal structure of lifts to .
Proof.
Again, denote by . The object and arrow categories are (braided, symmetric) monoidal by taking pointwise. The monoidal structure for -objects follows from that on and for -morphisms is
[TABLE]
Universal properties provide the associator, unitors, and coherence axioms. It is clear that is also braided or symmetric monoidal whenever is.
We obtain a monoidal structure for -objects by
[TABLE]
and for -morphisms by
[TABLE]
The monoidal unit for is the identity cospan on which is exactly . Universal properties again provide the associator, unitors, and coherence axioms. The braiding and symmetry of the monoidal structure clearly lifts from .
It is straightforward to check that the source and target functors are strict monoidal and respect the associator and unitors. It remains to find two invertible globular 2-cells: one witnessing interchange
[TABLE]
for -objects and , and another witnessing units
[TABLE]
for -arrows and . Moreover, and must satisfy certain axioms [40, Def. 2.9].
If , , , and , then has domain
[TABLE]
and codomain
[TABLE]
We must find a 2-cell whose outer square is formed by the domain and codomain of on the top and bottom plus identity -morphisms on the left and right. Let be the functor on the category
[TABLE]
whose image is of the form
[TABLE]
Then the domain of is and the codomain is . But these are isomorphic by assumption. This gives .
To define , let be the -morphism and let be . It is easy to check that both and are
[TABLE]
where the legs of the horizontal cospans are built using the inverses of the legs of and . The legs of the vertical spans are identities.
As for the remaining axioms, they are straightforward though tedious to check and are left to the reader. ∎
Lemma A.5**.**
* is isofibrant.*
Proof.
Take a vertical morphism . The legs of the companion , are the inverses of those from . The companion is equipped with the 2-morphisms
[TABLE]
The reader may check that the required equations hold. The conjoint of is . ∎
Theorem A.6**.**
* is a (braided, symmetric) monoidal bicategory.*
Proof.
Apply Theorem A.1. ∎
This proves the first half of Theorem 3.2. To prove the second half, we assume that is a cocartesian monoidal bicategory.
Note that we take Stay’s definition of a compact closed bicategory [41].
Lemma A.7**.**
The diagram
[TABLE]
in is a pushout square.
Proof.
Suppose form a cocone over the above diagram. Let be an inclusion into the middle copy of . Observe that and are the left and right inclusions . Then is a map , which we claim to be the unique map making the required diagram commute. Indeed, given such that , then . ∎
Theorem A.8**.**
* is compact closed.*
Proof.
The objects are self dual. To show this, start with an object . Define the evaluation morphism and coevaluation morphism by
[TABLE]
We next define the cusp isomorphisms, and . The domain for is the composite
[TABLE]
and the codomain for is
[TABLE]
That these are both identity cospans on follows from Lemma A.7 and the equations and Take and each to be the identity 2-morphism on . This gives a dual pair which we can complete to a coherent dual pair [37, p. 22]. ∎
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1]
- 2[2] S. Abramsky & B. Coecke (2004): A categorical semantics of quantum protocols . In: Logic in Computer Science. Proceedings of the 19th Annual IEEE Symposium , pp. 415–425, 10.1109/LICS.2004.1319636 . · doi ↗
- 3[3] Bob B. Coecke & B. Edwards (2011): Toy quantum categories . Electron. Notes Theor. Comput. Sci. 270(1), 10.1016/j.entcs.2011.01.004 . Available at https://arxiv.org/abs/0808.1037 . · doi ↗
- 4[4] M. Backens (2016): Completeness and the ZX-calculus , 10.1109/LICS.2004.1319636 . Available at https://arxiv.org/abs/1602.08954 . · doi ↗
- 5[5] J. Baez, B. Coya & F. Rebro (2017): Props in network theory . Available at https://arxiv.org/abs/1707.08321 .
- 6[6] J. Baez & B. Fong (2015): A compositional framework for passive linear networks . Available at https://arxiv.org/abs/1504.05625 .
- 7[7] J. Baez, B. Fong & B. Pollard (2016): A compositional framework for Markov processes . J. Math. Phys. 57, 10.1063/1.4941578 . · doi ↗
- 8[8] K. Bar, A. Kissinger & J. Vicary (2016): Globular: an online proof assistant for higher-dimensional rewriting . Available at http://globular.science .
