Structured cospans as a cocartesian equipment

applied category theory
double categories
systems theory
Author
Published

2023-03-15

Abstract

The theory of structured cospans is dramatically simplified by the use of double-categorical universal properties. Specifically, we show that structured cospans form a cocartesian equipment, a result that is stronger yet easier to prove than the usual result that they form a symmetric monoidal double category.

Structured cospans, along with their cousin decorated cospans, have become a standard tool to build categories of open systems () (). 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 () 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 () and symmetric monoidal bifibrations ().

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 (03 April 2023): I have incorporated the content of this blog post into a new paper ().

1 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 D\mathbb{D} is cocartesian if the underlying categories D0\mathbb{D}_0 and D1\mathbb{D}_1 have finite coproducts; the source and target functors s,t:D1D0s, t: \mathbb{D}_1 \to \mathbb{D}_0 preserve finite coproducts; and the external composition :D1×D0D1D1\odot: \mathbb{D}_1 \times_{\mathbb{D}_0} \mathbb{D}_1 \to \mathbb{D}_1 and external unit id:D0D1\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 D1\mathbb{D}_1.

Remark

A good reference for cartesian double categories is Aleiferi’s PhD thesis (). 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 (, Corollary 4.3.7). It is also instructive to prove this directly by unwinding the definitions.

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 D\mathbb{D} such that the source-target pairing s,t:D1D0×D0\langle s,t \rangle: \mathbb{D}_1 \to \mathbb{D}_0 \times \mathbb{D}_0 is a fibration. This means that every niche in D\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:xx{h: x' \to x} and k:yy{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 Csp(S)\mathbb{C}\mathsf{sp}(\mathsf{S}), the double category of cospans in a finitely cocomplete category S\mathsf{S}. Finite coproducts in the category Csp(S)0=S\mathbb{C}\mathsf{sp}(\mathsf{S})_0 = \mathsf{S} exist by assumption, and finite coproducts in the functor category Csp(S)1=S{}\mathbb{C}\mathsf{sp}(\mathsf{S})_1 = \mathsf{S}^{\{\bullet \rightarrow \bullet \leftarrow \bullet\}} are computed pointwise in S\mathsf{S}. So the source and target functors ftL,ftR:Csp(S)1S\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:

2 Double category of structured cospans

We now recall the main definitions of structured cospans. Given a finitely cocomplete category X\mathsf{X} and a functor L:AXL: \mathsf{A} \to \mathsf{X}, there is a double category of LL-structured cospans, denoted LCsp(X){}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X}), that has

  • as objects, the objects of A\mathsf{A};
  • as arrows, the morphisms of A\mathsf{A};
  • as proarrows with source aa and target bb, a cospan in X\mathsf{X} of form LaxLbLa \rightarrow x \leftarrow Lb;
  • as cells from (a,LaxLb,b)(a, La \rightarrow x \leftarrow Lb, b) to (c,LcyLd,d)(c, Lc \rightarrow y \leftarrow Ld, d) with source arrow f:ac{f: a \to c} and target arrow g:bd{g: b \to d}, a morphism of cospans in X\mathsf{X} of the form

Composition of arrows and cells in the categories LCsp(X)0{}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})_0 and LCsp(X)1{}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})_1 is by composition in A\mathsf{A} and Csp(X)1\mathbb{C}\mathsf{sp}(\mathsf{X})_1, respectively, and external composition of proarrows and cells is by pushout in X\mathsf{X}. It is easy to see that LL-structured cospans form a double category in this way since the double category structure is essentially inherited from that of cospans in X\mathsf{X}. For details, see ().

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 (). It was this study that motivated the thinking in this post. A generic implementation of structured cospans is provided by Catlab.jl.

3 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

Let X\mathsf{X} be a category with finite colimits and L:AXL: \mathsf{A} \to \mathsf{X} be any functor. Then the double category of LL-structured cospans is an equipment.

Proof. The restriction of an LL-structured cospan (c,LcyLd,d)(c, Lc \rightarrow y \leftarrow Ld, d) along arrows f:ac{f: a \to c} and g:bd{g: b \to d} in A\mathsf{A} is simply the restriction in the equipment Csp(X)\mathbb{C}\mathsf{sp}(\mathsf{X}) of the underlying cospan along LfLf and LgLg. The universal property holds as a special case of the universal property in Csp(X)\mathbb{C}\mathsf{sp}(\mathsf{X}):

For the double category of LL-structured cospans to be cocartesian, extra assumptions are needed. Clearly, the category A\mathsf{A} must itself have finite coproducts. Also, these must preserved by the functor L:AXL: \mathsf{A} \to \mathsf{X}. In practice, the latter is usually easy to verify by exhibiting LL as a left adjoint, which then preserves any colimits that exist in A\mathsf{A}.

Proposition

Let A\mathsf{A} be a category with finite coproducts, X\mathsf{X} be a category with finite colimits, and L:AXL: \mathsf{A} \to \mathsf{X} be a functor that preserves finite coproducts. Then the double category of LL-structured cospans is cocartesian.

Proof. By assumption, the category LCsp(X)0=A{}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})_0 = \mathsf{A} has finite coproducts. In the category X\mathsf{X}, which also has finite coproducts, there are canonical comparison maps

La,a:=[L(ιa),L(ιa)]:L(a)+L(a)L(a+a),a,aA, L_{a,a'} := [L(\iota_a), L(\iota_{a'})]: L(a) + L(a') \to L(a+a'), \qquad a, a' \in \mathsf{A},

and L0:0X!L(0A)L_0: 0_{\mathsf{X}} \xrightarrow{!} L(0_{\mathsf{A}}). For any maps f:acf:a \to c and f:acf': a' \to c in A\mathsf{A}, the comparison maps obey the equation

as can be seen by precomposing both sides with the coprojection ιLa\iota_{La} to obtain LfLf, and similarly for ιLa\iota_{La'} and LfLf'. Since LL preserves finite coproducts, the comparisons La,aL_{a,a'} and L0L_0 are, in fact, isomorphisms.

Consequently, the structured cospan (0A,idL(0A),0A)(0_{\mathsf{A}}, \operatorname{id}_{L(0_{\mathsf{A}})}, 0_{\mathsf{A}}) is initial in LCsp(X)1{}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})_1. As for binary coproducts, the coproduct (a+a, L(a+a)x+xL(b+b), b+b) (a+a',\ L(a+a') \rightarrow x+x' \leftarrow L(b+b'),\ b+b') of structured cospans (a,LaxLb,b){(a, La \rightarrow x \leftarrow Lb, b)} and (a,LaxLb,b){(a', La' \rightarrow x' \leftarrow Lb', b')} is obtained from the pointwise coproduct of cospans in Csp(X)\mathbb{C}\mathsf{sp}(\mathsf{X}) by restriction along La,a1L_{a,a'}^{-1} and Lb,b1L_{b,b'}^{-1}. The universal property in LCsp(X)1{}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X})_1 then takes the form

We have shown that both underlying categories of LCsp(X){}_{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 LCsp(X){}_{L}\mathbb{C}\mathsf{sp}(\mathsf{X}) relating coproducts and external composition are isomorphisms because they are defined by the same maps in X\mathsf{X} as the corresponding cells in Csp(X)\mathbb{C}\mathsf{sp}(\mathsf{X}), which we already know to be isomorphisms.

4 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 (), 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 (), (). 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 (). 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

Aduddell, Rebekah, James Fairbanks, Amit Kumar, Pablo S. Ocal, Evan Patterson, and Brandon T. Shapiro. 2023. “A Compositional Account of Motifs, Mechanisms, and Dynamics in Biochemical Regulatory Networks.” https://arxiv.org/abs/2301.01445.
Aleiferi, Evangelia. 2018. “Cartesian Double Categories with an Emphasis on Characterizing Spans.” PhD thesis, Dalhousie University. https://arxiv.org/abs/1809.06940.
Baez, John C., and Kenny Courser. 2020. “Structured Cospans.” Theory and Applications of Category Theory 35 (48): 1771–1822. http://www.tac.mta.ca/tac/volumes/35/48/35-48abs.html.
Baez, John C., Kenny Courser, and Christina Vasilakopoulou. 2022. “Structured Versus Decorated Cospans.” Compositionality 4 (3). https://doi.org/10.32408/compositionality-4-3.
Courser, Kenny. 2020. “Open Systems: A Double Categorical Perspective.” PhD thesis, University of California, Riverside. https://escholarship.org/uc/item/7b41h3s3.
Fiadeiro, José Luiz, and Vincent Schmitt. 2007. “Structured Co-Spans: An Algebra of Interaction Protocols.” In International Conference on Algebra and Coalgebra in Computer Science (CALCO 2007), 194–208. https://doi.org/10.1007/978-3-540-73859-6_14.
Fong, Brendan, and David I. Spivak. 2019. “Hypergraph Categories.” Journal of Pure and Applied Algebra 223 (11): 4746–77. https://doi.org/10.1016/j.jpaa.2019.02.014.
Grandis, Marco. 2019. Higher Dimensional Categories: From Double to Multiple Categories. World Scientific. https://doi.org/10.1142/11406.
Lambert, Michael. 2022. “Double Categories of Relations.” Theory and Applications of Categories 38 (33): 1249–83. http://www.tac.mta.ca/tac/volumes/38/33/38-33abs.html.
Patterson, Evan. 2023. “Structured and Decorated Cospans from the Viewpoint of Double Category Theory.” In Applied Category Theory 2023. https://arxiv.org/abs/2304.00447.
Leaving a comment will set a cookie in your browser. For more information, see our cookies policy.