We define a notion of symmetric monoidal closed (SMC) theory, consisting of a SMC signature augmented with equations, and describe the classifying categories of such theories in terms of proof nets.
Milners bigraphs are a general framework for reasoning about distributed and concurrent programming languages. Notably, it has been designed to encompass both the pi-calculus and the Ambient calculus. This paper is only concerned with bigraphical syn
tax: given what we here call a bigraphical signature K, Milner constructs a (pre-) category of bigraphs BBig(K), whose main features are (1) the presence of relative pushouts (RPOs), which makes them well-behaved w.r.t. bisimulations, and that (2) the so-called structural equations become equalities. Examples of the latter include, e.g., in pi and Ambient, renaming of bound variables, associativity and commutativity of parallel composition, or scope extrusion for restricted names. Also, bigraphs follow a scoping discipline ensuring that, roughly, bound variables never escape their scope. Here, we reconstruct bigraphs using a standard categorical tool: symmetric monoidal closed (SMC) theories. Our theory enforces the same scoping discipline as bigraphs, as a direct property of SMC structure. Furthermore, it elucidates the slightly mysterious status of so-called links in bigraphs. Finally, our category is also considerably larger than the category of bigraphs, notably encompassing in the same framework terms and a flexible form of higher-order contexts.
We show how to construct a Gamma-bicategory from a symmetric monoidal bicategory, and use that to show that the classifying space is an infinite loop space upon group completion. We also show a way to relate this construction to the classic Gamma-cat
egory construction for a bipermutative category. As an example, we use this machinery to construct a delooping of the K-theory of a bimonoidal category as defined by Baas-Dundas-Rognes.
In previous work we proved that, for categories of free finite-dimensional modules over a commutative semiring, linear compact-closed symmetric monoidal structure is a property, rather than a structure. That is, if there is such a structure, then it
is uniquely defined (up to monoidal equivalence). Here we provide a novel unifying category-theoretic notion of symmetric monoidal structure with local character, which we prove to be a property for a much broader spectrum of categorical examples, including the infinite-dimensional case of relations over a quantale and the non-free case of finitely generated modules over a principal ideal domain.
We give a complete presentation for the fragment, ZX&, of the ZX-calculus generated by the Z and X spiders (corresponding to copying and addition) along with the not gate and the and gate. To prove completeness, we freely add a unit and counit to the
category TOF generated by the Toffoli gate and ancillary bits, showing that this yields the full subcategory of finite ordinals and functions with objects powers of two; and then perform a two way translation between this category and ZX&. A translation to some extension of TOF, as opposed to some fragment of the ZX-calculus, is a natural choice because of the multiplicative nature of the Toffoli gate. To this end, we show that freely adding counits to the semi-Frobenius algebras of a discrete inverse category is the same as constructing the Cartesian completion. In particular, for a discrete inverse category, the category of classical channels, the Cartesian completion and adding counits all produce the same category. Therefore, applying these constructions to TOF produces the full subcategory of finite ordinals and partial maps with objects powers of two. By glueing together the free counit completion and the free unit completion, this yields qubit multirelations.
Applications of category theory often involve symmetric monoidal categories (SMCs), in which abstract processes or operations can be composed in series and parallel. However, in 2020 there remains a dearth of computational tools for working with SMCs
. We present an unbiased approach to implementing symmetric monoidal categories, based on an operad of directed, acyclic wiring diagrams. Because the interchange law and other laws of a SMC hold identically in a wiring diagram, no rewrite rules are needed to compare diagrams. We discuss the mathematics of the operad of wiring diagrams, as well as its implementation in the software package Catlab.