The n-Category Café

Yes, that does look like essentially the same idea. Doing it in three dimensions also seems to make it easier to see what’s happening when composing functors, although it’s probably harder to draw that way in the computer.

Do you know of Charles Peirce’s existential graph approach to logic? Your modus ponens diagram looks very like how you would render his version (see, e.g., half way down here) in 3D.

From your mention of ‘Laws of Form’ perhaps you have looked more at Spencer-Brown. If I recall correctly, his system was very close to Peirce’s, but juxtaposition of proposition letters signified ‘or’ rather than ‘and’.

Todd Trimble would be able to tell us more. See his papers with Geraldine Brady.

Thanks for taking a stab at this! Sorry for the delayed response.

The rules of fibrations are easy to imagine.

Not to me; I don’t think I understand what you have in mind. I gather that you want to apply the graphical calculus of monoidal functors to the fibration $\Phi\colon E\to B$, which is great, but I don’t see how to notate the operation of pullback along cartesian arrows. For instance, how would you notate the object $\Delta_x^*(a\boxtimes b)$ which defines the “fiberwise” tensor product?

I think it’s very different, for the same reasons that MonCat is not a full sub-3-category of Bicat. A monoidal functor between monoidal categories is the same as a 2-functor between their deloopings, but saying that the monoidal functor is a fibration is about liftings of 1-morphisms, which becomes lifting of 2-morphisms in the delooping. But saying that a 2-functor is a 2-fibration entails not only lifting of 2-morphisms, but also lifting of 1-morphisms.

Thus, if $\Phi\colon E\to B$ is a monoidal functor, then for its delooping to be a 2-fibration it would have to be the case that for any object $x\in B$, there is an object $a\in E$ with $\Phi(a)=x$ (or $\cong x$) such that for any $b\in E$ with $\Phi(b) = y\otimes x$ (or $\cong$), there exists a unique (maybe up to isomorphism) object $c\in E$ with $\Phi(c) = y$ and $b = c\otimes a$. This is kind of a weird property, and I don’t think it holds in any of the examples I’m interested in.

That’s a good idea; that expression of predicate calculus is a very good example of a monoidal fibration. (Actually, once you have monoidal fibers, the functors $\boxtimes$ come for free as I sketched above; they end up being conjuction with contexts made disjoint.) And now that you link to it, I dimly remember skimming through the Brady-Trimble paper a long time ago. Actually, it probably influenced my early thinking about monoidal fibrations and framed bicategories, although I had forgotten it until now.

It seems as though their string diagrams consist essentially of first making the monoidal fibration into a locally-posetal compact-closed 2-category (which is the horizontal 2-category of the double category that can be constructed from any suitable monoidal fibration), and then using ordinary-ish monoidal-category string diagrams there (with surgeries on string diagrams to represent the 2-cells). Is that accurate? (I’m ignoring things like sep lines which seem specific to classical predicate calculus, versus general monoidal fibrations.)

If my understanding is right, then it is sort of an answer to my question, but I’m not sure how I feel about it. I’d have to try working with it for a bit to see how convenient it is. One problem is that in the non-posetal case, surgeries don’t seem quite as convenient a way to represent the 2-cells, since you need to label them with which 2-cell they represent and give rules for when two surgeries should be considered equal. (Probably that is an indication that we really need to move up a dimension and use real surface diagrams for monoidal 2-categories.)

I’d also kind of hoped for a more “native” string diagram calculus for monoidal fibrations, which one could use (among other things) to prove things like that you can construct a compact-closed double category from any monoidal fibration, rather than building that fact into the string diagram calculus. In particular, it’s not immediately clear whether these string diagrams could be generalized to monoidal fibrations lacking pushforwards (existential quantification), since pushforwards are required to get a double category (although you can get a virtual double category in general…).

Regardless, this is a really interesting approach, and I need to think about it some more.

Coincidentally, in a discussion of string diagrams for closed monoidal categories on the categories list, Peter Selinger recently concluded

I guess the point is that one can save some time by exploiting what logicians have already done, using the connections between logic, category theory, and string diagrams, rather than re-inventing the wheel.

Thinking about this overnight, I realized that there are “native” string diagrams for monoidal fibrations sitting inside those for the monoidal 2-category, and these can be described directly even when pushforwards are missing or the base is not cartesian. These are the string diagrams with no strings coming out the bottom, i.e. whose target is the unit object. Reading carefully, I see that Brady-Trimble singled these out as well, calling them “positive geometric formulas” (p17) — I guess that indicates that those are also (closer to) the ones that Pierce originally described.

So in the graphical calculus that I’m now seeing for a monoidal fibration $\Phi:E\to B$, an object of $E$ is represented by a string diagram, with no strings coming out the bottom, with strings labeled by objects of $B$, and with two types of nodes: (1) objects of $E$, which have empty target and a source labeled with their image under $\Phi$, and (2) morphisms of $B$, which have source and target just as in ordinary string diagrams for $B$. The “value” of this string diagram is given by tensoring together all the objects of $E$ which occur in it, then pulling back along a suitable morphism of $B$ built from all those occurring in the diagram. The morphisms of $E$ are then represented by surface diagrams relating these string diagrams.

This version seems to solve all my initial complaints! I need to spend a while working with it to get used to it, but it may be exactly what I was looking for. I’m a little scared by the appearance of surface diagrams, but probably we’re up high enough in dimensions here that something of that sort is inevitable.