September 20, 2018

Cartesian Double Categories

Posted by Mike Shulman

In general, there are two kinds of bicategories: those like $Cat$ and those like $Span$. In the $Cat$-like ones, the morphisms are “categorified functions”, which generally means some kind of “functor” between some kind of “category”, consisting of functions mapping objects and arrows from domain to codomain. But in the $Span$-like ones (which includes $Mod$ and $Prof$), the morphisms are not “functors” but rather some kind of “generalized relations” (including spans, modules, profunctors, and so on) which do not map from domain to codomain but rather relate the domain and codomain in some way.

In $Span$-like bicategories there is usually a subclass of the morphisms that do behave like categorified functions, and these play an important role. Usually the morphisms in this subclass all have right adjoints; sometimes they are exactly the morphisms with right adjoints; and often one can get away with talking about “morphisms with right adjoints” rather than making this subclass explicit. However, it’s also often conceptually and technically helpful to give the subclass as extra data, and arguably the most perspicuous way to do this is to work with a double category instead. This was the point of my first published paper, though others had certainly made the same point before, and I think more and more people are coming to recognize it.

Today a new installment in this story appeared on the arXiv: Cartesian Double Categories with an Emphasis on Characterizing Spans, by Evangelia Aleiferi. This is a project that I’ve wished for a while someone would do, so I’m excited that at last someone has!

We know now that various structure on a double category corresponds to similar structure on a bicategory. For instance, a monoidal structure on a (suitably well-behaved) double category induces a monoidal structure on its underlying bicategory. However, the monoidal double category is generally much stricter and easier to work with.

Aleiferi’s paper is about extending this to the cartesian monoidal case. A cartesian monoidal double category is easy to define: its diagonal $D\to D\times D$ and projection $D\to 1$ have right adjoints, just as for ordinary categories. It’s also easy to say what it means for a $Cat$-like bicategory to be cartesian monoidal: we can say that its diagonal and projection have right adjoints too, although that’s more complicated because the adjoints are generally only pseudofunctors living in a tricategory.

But it’s not at all obvious what it means for a $Span$-like bicategory to be “cartesian monoidal”. Intuitively, bicategories like $Span$ itself, or more generally $Span(E)$ for $E$ a category with finite limits, and $Prof(V)$ when $V$ is cartesian monoidal, should be “cartesian” — but they are not cartesian monoidal in the $Cat$-like way. The notion of cartesian bicategory was defined (by Carboni, Walters, Kelly, Verity, and Wood) to capture examples like these, but it is quite complicated. Moreover, to someone familiar with double categories, it is crying out to be reformulated in double-category language (e.g. it requires certain morphisms to have right adjoints, and induces $Cat$-like cartesian structure on the sub-bicategory of morphisms with right adjoints). In fact, it blows my mind that anyone was able to define the notion of cartesian bicategory without secretly having double categories in their head!

Aleiferi has now made a more careful study of cartesian double categories, and shown that they can be used for at least some (which I suspect will eventually become “nearly all”) of the same purposes as cartesian bicategories. For instance, here is a theorem from Lack-Walters-Wood Bicategories of spans as cartesian bicategories:

Theorem: A bicategory is equivalent to $Span(E)$, for some category $E$ with finite limits, if and only if it is cartesian, each comonad has an Eilenberg-Moore object, and every map is comonadic.

And here is a theorem from Aleiferi’s paper:

Theorem: A double category is equivalent to $Span(E)$, for some category $E$ with finite limits, if and only if it is cartesian, fibrant, unit-pure, and has strong Eilenberg-Moore objects for copointed endomorphisms.

Even without understanding all the words, the family resemblance should be clear, even if the technicalities are different. On a quick skim of Aleiferi’s paper it looks like there is no formal comparison yet between cartesian double categories and cartesian bicategories, but I’m sure that will come.

Posted at September 20, 2018 7:22 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3061

Re: Cartesian double categories

…they can be used for at least some (which I suspect will eventually become “nearly all”) of the same purposes as cartesian bicategories

Coincidently I’ve just heard Jens Seeber on cartesian bicategories used for Graphical conjunctive queries, which appear in database theory. Could cartesian double categories play a role here?

Posted by: David Corfield on September 21, 2018 11:41 AM | Permalink | Reply to this

Re: Cartesian double categories

Probably! The bicategory $Rel$ is, of course, the underlying bicategory of a double category, whose additional morphisms are functions. I haven’t done more than glance at their paper, but it seems to involve also spans and cospans, both of which form double categories, and we’ve recently seen how the double-categorical viewpoint on such things can be useful.

(That PDF exhibits an interesting failure of the arXiv watermarking which I haven’t encountered before. Must be an interaction with some rare document class or package?)

Posted by: Mike Shulman on September 21, 2018 8:44 PM | Permalink | Reply to this

Re: Cartesian double categories

…the use of diagrammatic reasoning as a powerful method of logical reasoning actually go back to the pre-Frege work of the 19th century American polymath CS Peirce on existential graphs. Interestingly, it is only recently (see, e.g. [30]) that this work has been receiving the attention that it richly deserves.

Hmm.

Frege’s Begriffsschrift was published in 1879. Existential graphs replaced Entitative graphs and even the latter hadn’t surfaced by 1879.

As for the second claim, [30] is Melliès and Zeilberger’s A bifibrational reconstruction of Lawvere’s presheaf hyperdoctrine from 2016.

In the 90s I remember reading

• Roberts, Don, 1973, The Existential Graphs of Charles S. Peirce, The Hague: Mouton.

Roberts and Jay Zeman were on the case at least as early as 1964.

And if we’re only interested in category theoretic treatments, try the Brady and Trimble papers from 2000 listed here.

Posted by: David Corfield on September 22, 2018 10:16 AM | Permalink | Reply to this

Re: Cartesian double categories

By “pre-Frege” we were referring to what people normally consider as the modern notation for Frege quantifiers (i.e. ∀ and ∃). Interestingly, Frege himself used a graphical notation in 1879.

Admittedly, this is somewhat clumsily written, due partly to space restrictions. Apologies.

We were aware of the work Brady and Trimble and the earlier works, such as Roberts and Zeman. Nevertheless, this was––to quote Brady and Trimble–an “obscure topic.” The point of giving a 2016 reference was that in the last two years I’ve heard many people talk about existential graphs: they are somehow in the air. Deservedly so, I think.

Posted by: Pawel Sobocinski on September 28, 2018 11:45 AM | Permalink | Reply to this

Re: Cartesian double categories

Well then, if Wikipedia is to be believed, your “pre-Frege” is any time before 1960.

In 1935, Gentzen introduced the ∀ symbol, by analogy with Peano’s ∃ symbol. ∀ did not become canonical until the 1960s.

I’ve added your article to those who have revived existential graphs at nLab: Charles Sanders Peirce. The entry is in serious need of construction.

Posted by: David Corfield on September 28, 2018 1:21 PM | Permalink | Reply to this

Re: Cartesian double categories

Would you be happy with “pre-dating the Frege-Goedel-Gentzen tradition of mathematical logic”?

Posted by: Pawel Sobocinski on September 28, 2018 2:26 PM | Permalink | Reply to this

Re: Cartesian double categories

Well, identifying traditions is no easy business, especially over extended time periods. Over a briefer period Zeman reasonably claims:

Peirce developed independently of the Frege-Peano-Russell (FPR) tradition all of the key formal logical results of that tradition. He did this first in an algebraic format similar to that employed later in Principia Mathematica and then, for philosophical reasons founded in the theory of signs, he became dissatisfied with algebraic notation for logic; this dissatisfaction resulted in his development of a successful graphical logical notation; in his work in this notation (his “Existential Graphs”) he anticipated philosophically important extensions of basic mathematical logic which eluded independent rediscovery till after the middle of this century.

This is also cited at the end of Anellis’s How Peircean was the “‘Fregean’ Revolution” in Logic? which appears to be a very useful resource for understanding developments and influences in the early years of predicate logic. Note that Russell had read Peirce, so one would need to be cautious in maintaining too complete a picture of the independence of such an “FPR tradition” from him.

Posted by: David Corfield on September 29, 2018 7:55 AM | Permalink | Reply to this

Re: Cartesian double categories

One more related question – how do the string diagrams of Myers for double categories and equipments relate to those of this paper?

Posted by: David Corfield on September 22, 2018 10:49 AM | Permalink | Reply to this

Re: Cartesian double categories

I don’t know, I’m not sure exactly how their graphical language corresponds to the categories in question here.

Posted by: Mike Shulman on September 22, 2018 11:26 AM | Permalink | Reply to this

Re: Cartesian double categories

Unless I’m mistaken this paper seems to use conventional “square” diagrams for double categories and Myers’ diagrams are a Poincare dual of that so more like string diagrams. Myers talks about this in their paper

Posted by: Max S New on September 22, 2018 2:41 PM | Permalink | Reply to this

Re: Cartesian double categories

Is that right? Aren’t they both on the dual side? Their diagrams closely resemble Brady and Trimble’s in A string diagram calculus for predicate logic with relation symbols marking nodes joining strings representing elements.

Posted by: David Corfield on September 22, 2018 3:51 PM | Permalink | Reply to this

Re: Cartesian double categories

We use the usual notion of string diagram for strict monoidal categories, read from left-to-right. They themselves are a specialisation of string diagrams for 2-categories to the one object case. This tradition goes back a long time, but as far as I know, they were first formalised by Joyal and Street in 1991.

However, in our papers we normally don’t think of them as topological objects but as (equivalence classes of) syntactic objects, built up of basic components by the operations of monoidal categories. That is, as terms of symmetric monoidal theories, generalising Lawvere theories.

I learned this more “computer-sciency” way of looking at string diagrams from RFC Walters and his string diagrams (e.g. in papers on Span(Graph)) are drawn in this style. So, in computations, while topological deformation and diagrammatic reasoning give the intuitions, formally what’s going on is 2-dimensional term-rewriting.

Posted by: Pawel Sobocinski on September 28, 2018 12:27 PM | Permalink | Reply to this

Post a New Comment