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 \(\mathbb{D}\) is cocartesian1 if the underlying categories \(\mathbb{D}_0\) and \(\mathbb{D}_1\) have finite coproducts; the source and target functors \(s, t: \mathbb{D}_1 \to \mathbb{D}_0\) preserve finite coproducts; and the external composition \(\odot: \mathbb{D}_1 \times_{\mathbb{D}_0} \mathbb{D}_1 \to \mathbb{D}_1\) and external unit \(\operatorname{id}: \mathbb{D}_0 \to \mathbb{D}_1\) also preserve finite coproducts, meaning that the canonical comparison cells
and
given by the universal properties of binary coproducts and initial objects, are all isomorphisms in \(\mathbb{D}_1\).
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 \(\mathbb{D}\) such that the source-target pairing \(\langle s,t \rangle: \mathbb{D}_1 \to \mathbb{D}_0 \times \mathbb{D}_0\) is a fibration. This means that every niche in \(\mathbb{D}\) of the form on the left can be completed to a cell as on the right
called a restriction cell, with the universal property that for every pair of arrows \({h: x' \to x}\) and \({k: y' \to y}\), each cell \(\alpha\) of the form on the left factors uniquely through the restriction cell as on the right:
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 \(\mathbb{C}\mathsf{sp}(\mathsf{S})\), the double category of cospans in a finitely cocomplete category \(\mathsf{S}\). Finite coproducts in the category \(\mathbb{C}\mathsf{sp}(\mathsf{S})_0 = \mathsf{S}\) exist by assumption, and finite coproducts in the functor category \(\mathbb{C}\mathsf{sp}(\mathsf{S})_1 = \mathsf{S}^{\{\bullet \rightarrow \bullet \leftarrow \bullet\}}\) are computed pointwise in \(\mathsf{S}\). So the source and target functors \(\operatorname{ft}_L, \operatorname{ft}_R: \mathbb{C}\mathsf{sp}(\mathsf{S})_1 \to \mathsf{S}\), extracting the left and right feet, preserve coproducts. The comparison cells are isomorphisms because colimits commute with colimits (specifically, pushouts commute with coproducts) up to canonical isomorphism. The double category of cospans is thus cocartesian. It is also an equipment. To restrict a cospan along a pair of morphisms, simply compose them with the legs of the cospan to obtain a new cospan with the same apex:
Double category of structured cospans
We now recall the main definitions of structured cospans. Given a finitely cocomplete category \(\mathsf{X}\) and a functor \(L: \mathsf{A} \to \mathsf{X}\), there is a double category of \(L\)-structured cospans, denoted \({}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})\), that has
- as objects, the objects of \(\mathsf{A}\);
- as arrows, the morphisms of \(\mathsf{A}\);
- as proarrows with source \(a\) and target \(b\), a cospan in \(\mathsf{X}\) of form \(La \rightarrow x \leftarrow Lb\);
- as cells from \((a, La \rightarrow x \leftarrow Lb, b)\) to \((c, Lc \rightarrow y \leftarrow Ld, d)\) with source arrow \({f: a \to c}\) and target arrow \({g: b \to d}\), a morphism of cospans in \(\mathsf{X}\) of the form
Composition of arrows and cells in the categories \({}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})_0\) and \({}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})_1\) is by composition in \(\mathsf{A}\) and \(\mathbb{C}\mathsf{sp}(\mathsf{X})_1\), respectively, and external composition of proarrows and cells is by pushout in \(\mathsf{X}\). It is easy to see that \(L\)-structured cospans form a double category in this way since the double category structure is essentially inherited from that of cospans in \(\mathsf{X}\). For details, see (Baez and Courser 2020, sec. 2).
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 \(\mathsf{X}\) be a category with finite colimits and \(L: \mathsf{A} \to \mathsf{X}\) be any functor. Then the double category of \(L\)-structured cospans is an equipment.
Proof. The restriction of an \(L\)-structured cospan \((c, Lc \rightarrow y \leftarrow Ld, d)\) along arrows \({f: a \to c}\) and \({g: b \to d}\) in \(\mathsf{A}\) is simply the restriction in the equipment \(\mathbb{C}\mathsf{sp}(\mathsf{X})\) of the underlying cospan along \(Lf\) and \(Lg\). The universal property holds as a special case of the universal property in \(\mathbb{C}\mathsf{sp}(\mathsf{X})\):
For the double category of \(L\)-structured cospans to be cocartesian, extra assumptions are needed. Clearly, the category \(\mathsf{A}\) must itself have finite coproducts. Also, these must preserved by the functor \(L: \mathsf{A} \to \mathsf{X}\). In practice, the latter is usually easy to verify by exhibiting \(L\) as a left adjoint, which then preserves any colimits that exist in \(\mathsf{A}\).
Proposition 2 Let \(\mathsf{A}\) be a category with finite coproducts, \(\mathsf{X}\) be a category with finite colimits, and \(L: \mathsf{A} \to \mathsf{X}\) be a functor that preserves finite coproducts. Then the double category of \(L\)-structured cospans is cocartesian.
Proof. By assumption, the category \({}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})_0 = \mathsf{A}\) has finite coproducts. In the category \(\mathsf{X}\), which also has finite coproducts, there are canonical comparison maps
\[ L_{a,a'} := [L(\iota_a), L(\iota_{a'})]: L(a) + L(a') \to L(a+a'), \qquad a, a' \in \mathsf{A}, \]
and \(L_0: 0_{\mathsf{X}} \xrightarrow{!} L(0_{\mathsf{A}})\). For any maps \(f:a \to c\) and \(f': a' \to c\) in \(\mathsf{A}\), the comparison maps obey the equation
as can be seen by precomposing both sides with the coprojection \(\iota_{La}\) to obtain \(Lf\), and similarly for \(\iota_{La'}\) and \(Lf'\). Since \(L\) preserves finite coproducts, the comparisons \(L_{a,a'}\) and \(L_0\) are, in fact, isomorphisms.
Consequently, the structured cospan \((0_{\mathsf{A}}, \operatorname{id}_{L(0_{\mathsf{A}})}, 0_{\mathsf{A}})\) is initial in \({}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})_1\). As for binary coproducts, the coproduct
\[ (a+a',\ L(a+a') \rightarrow x+x' \leftarrow L(b+b'),\ b+b') \]
of structured cospans \({(a, La \rightarrow x \leftarrow Lb, b)}\) and \({(a', La' \rightarrow x' \leftarrow Lb', b')}\) is obtained from the pointwise coproduct of cospans in \(\mathbb{C}\mathsf{sp}(\mathsf{X})\) by restriction along \(L_{a,a'}^{-1}\) and \(L_{b,b'}^{-1}\). The universal property in \({}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})_1\) then takes the form
We have shown that both underlying categories of \({}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})\) have finite coproducts, and it is immediate that the source and target functors preserve them.
Finally, the comparison cells in \({}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})\) relating coproducts and external composition are isomorphisms because they are defined by the same maps in \(\mathsf{X}\) as the corresponding cells in \(\mathbb{C}\mathsf{sp}(\mathsf{X})\), which we already know to be isomorphisms.
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.↩︎