Structured cospans as a cocartesian equipment
This post is cross-posted at the Topos Institute blog.
Structured cospans, along with their cousin decorated cospans, have become a standard tool to build categories of open systems (Fiadeiro and Schmitt 2007; Baez and Courser 2020). Compared with other techniques, structured cospans have the advantage of being particularly easy to use, as the hypotheses for the construction are often easy to check in practice. However, the proof that the construction itself works is rather involved because the mathematical object being constructed—a symmetric monoidal double category—is inherently complicated, involving a large number of diagrams that must commute. Three different correctness proofs for structured cospans have been given: the first one by direct but lengthy verification of the axioms (Courser 2020) and the two later ones by more conceptual routes that however import other sophisticated concepts. These concepts are pseudocategories in the 2-category of symmetric monoidal categories (Baez and Courser 2020) and symmetric monoidal bifibrations (Baez, Courser, and Vasilakopoulou 2022).
The thesis of this post is that such difficulties can be bypassed by viewing structured cospans in a different light, as forming a cocartesian double category. Just as a cartesian or cocartesian category can be given the structure of a symmetric monoidal category by making a choice of finite products or coproducts, so can a cartesian or cocartesian double category be given the structure of a symmetric monoidal double category. We will also show that structured cospans form an equipment, also called a fibrant double category, so altogether form a cocartesian equipment. This fact is significant because the most fundamental double categories, such as those of spans, matrices, relations, profunctors, and cospans, tend to be cartesian or cocartesian equipments or both.
Being a cocartesian equipment is a stronger result than being a symmetric monoidal double category, yet it is easier to prove. Far from being paradoxical, this situation highlights a recurring tension in category theory: that between universal properties and algebraic structures. Although algebraic structure is arguably more flexible, universal properties, when they can be found, are extremely powerful because many consequences and coherences flow directly from the defining existence and uniqueness statement, which is often easy to verify in examples. In this case, both cocartesian double categories and equipments are defined by universal properties, whereas a symmetric monoidal product is a structure on a double category.
Update (April 3, 2023): I have incorporated the content of this blog post into a new paper (Patterson 2023).
Cocartesian equipments
We begin by reviewing the definition of a cocartesian double category, which is not as well known as it should be. Just as a cocartesian category is (on one definition) a category with finite coproducts, a cocartesian double category is a double category with finite double-categorical coproducts. Unless you already have a good understanding of double-categorical colimits, that definition is not very helpful, so we provide the following more concrete description.
A double category
and
given by the universal properties of binary coproducts and initial objects, are all isomorphisms in
An equipment, also known as a fibrant double category or a framed bicategory, is a double category in which proarrows can be restricted or extended along pairs of arrows in a universal way. This can defined precisely in several equivalent ways, of which the following is most convenient for us. An equipment is a double category
called a restriction cell, with the universal property that for every pair of arrows
Finally, a cocartesian equipment is simply a double category that is both cocartesian and an equipment. We emphasize again that being a cocartesian equipment is a property of, not a structure on, a double category.
The prototypical example of a cocartesian equipment is none other than
Double category of structured cospans
We now recall the main definitions of structured cospans. Given a finitely cocomplete category
- as objects, the objects of
; - as arrows, the morphisms of
; - as proarrows with source
and target , a cospan in of form ; - as cells from
to with source arrow and target arrow , a morphism of cospans in of the form
Composition of arrows and cells in the categories
Structured cospans are now widely used in applied category theory. Besides the original literature, a number of applications of structured cospans—to open graphs, open categories, and open parameterized dynamical systems—can be found in our recent paper on the mathematics of biochemical regulatory networks (Aduddell et al. 2023). It was this study that motivated the thinking in this post. A generic implementation of structured cospans is provided by Catlab.jl.
Cocartesian equipment of structured cospans
With all the relevant definitions in hand, we now prove that structured cospans form an equipment, then a cocartesian double category, and hence a cocartesian equipment.
Proposition 1 Let
Proof. The restriction of an
For the double category of
Proposition 2 Let
Proof. By assumption, the category
and
as can be seen by precomposing both sides with the coprojection
Consequently, the structured cospan
of structured cospans
We have shown that both underlying categories of
Finally, the comparison cells in
Discussion
The brevity and simplicity of these proofs shows the benefits of viewing structured cospans as a cocartesian equipment. A natural next step would be to treat maps between double categories of structured cospans in the same way. In (Baez and Courser 2020, sec. 4), these maps are taken to be symmetric monoidal double functors and the proofs are omitted for being too long and tedious to record. It should instead be possible to give short, simple proofs that there are cocartesian double functors between cocartesian double categories of structured cospans, since one only needs to check that the canonical comparisons are isomorphisms.
Another result known about the double category of structured cospans is that it decategorifies, by taking globular isomorphism classes of proarrows, into a hypergraph category (Fong and Spivak 2019; Baez and Courser 2020). This result does not seem to be true of an arbitrary cartesian or cocartesian equipment, as it depends on the Frobenius law relating the companions and conjoints of the (co)multiplication maps. A locally posetal cartesian equipment satisfying the Frobenius law has been called a double category of relations (Lambert 2022). As far as I know, general axioms for the double-categorical analogue of a hypergraph category have not been worked out.
In a previous blog post, we showed that decorated cospans are an example of the double-categorical Grothendieck construction. Taken together, this series of posts provides further evidence that the use of double categories in studying open systems is not incidental, nor merely a means to construct categories or bicategories, but offers fundamental insights that cannot be obtained at the 1-categorical or even bicategorical levels.
References
Footnotes
A good reference for cartesian double categories is Aleiferi’s PhD thesis (Aleiferi 2018). The dual of the definition there is not obviously equivalent to the one just given, but their equivalence follows from a general theorem about double adjunctions (Grandis 2019, Corollary 4.3.7). It is also instructive to prove this directly by unwinding the definitions.↩︎