You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Aaron David Fairbanks (Sep 29 2022 at 19:00):A (colored) prop is called "representable" when each list of objects in the prop is isomorphic to a single object.
It seems to me most people who like props are aware of the fact that representable props are equivalent to symmetric monoidal categories.
This appears as Theorem 2.3 in Mike Shulman's A practical type theory for symmetric monoidal categories . This paper is the only reference I know for this fantastic result or any result like it. Does anyone know the history of analogous theorems about the equivalence between representable prop-like structures and weak 2-categorical structures?
For similar reasons, it seems monoidal categories are equivalent to representable pros.
Likewise, it seems bicategories are equivalent to representable "pros with colored regions".
What about double categories?
Consider a structure X defined by the analogy monoidal category : pro :: double category : X. This structure X is like a double category, except its 1-cells cannot compose (neither vertically nor horizontally), and its 2-cells are bordered by pasting diagrams of 1-cells rather than single 1-cells.
Are doubly weak double categories equivalent to Xs that are both vertically and horizontally representable? Is this a good way to first wrap my head around doubly weak double categories?
Amar Hadzihasanovic (Sep 29 2022 at 19:18):Hermida's Representable multicategories is the standard reference for the general setup, there instantiated for the equivalence between monoidal categories and representable multicategories. But the idea is already present in Cockett and Seely's papers on linearly distributive categories (equivalent to polycategories “representable on both sides”). There is also a version “with coloured regions”: linear bicategories are equivalent to representable poly-bicategories
For people who are acquainted with this branch of “Canadian” category theory, I think the result about pros and props are mostly understood as degenerate versions of the result for polycategories: if a representable polycategory extends to a prop, then the “tensor” and “par” of the corresponding linearly distributive category collapse to a single operation, so the linearly distributive category is “actually” a monoidal category.
I think this fact -- that the “representable prop” result is a “degenerate case” of a more refined result about polycategories -- may be why the prop result is hard to find in publications (I have also only seen it spelled out in Shulman's paper that you cite).
Amar Hadzihasanovic (Sep 29 2022 at 19:20):More troublingly, the relevance of this result to the theory of string diagrams seems to be little known in the string diagram community, which has led to parts of it being “rediscovered” over and over... I am actually writing an expository paper for this purpose.
Amar Hadzihasanovic (Sep 29 2022 at 19:20):Unfortunately, I don't know an answer to your question about double categories :)
Aaron David Fairbanks (Sep 29 2022 at 19:37):Ah, thank you for all this!
I agree, I see this as a very useful result. I've specifically gotten a lot of mileage out of thinking of 2-categorical structures as representable "many-in, many-out" prop-like structures (more than multicategory-like structures) because representability is so neatly described in terms of existence of isomorphisms within the structure.
Good luck with your expository paper!
Mike Shulman (Sep 29 2022 at 20:26):Regarding double categories, this is actually something I spent a while thinking about! In fact, I have a half-written paper lying around waiting to be completed (or superseded). This definition of doubly-weak double category isn't in the literature, so far as I know, but I believe it's the best one.
Mike Shulman (Sep 29 2022 at 20:26):There is an extra subtlety in that not every "arrangement of rectangles" is actually composable in a double category: as shown by Dawson there are "pinwheel" shapes that can't be decomposed into the binary composites available in the standard definition of double category. So in defining prop-like double-category structures (at one time I planned to call them "double caterads") you have to decide whether to allow "pinwheel composites".
Mike Shulman (Sep 29 2022 at 20:28):I think a nice way to construct and compare double-categorical structures is in terms of monads on the category of double computads, which have objects, two kinds of arrows without compositions, and 2-cells with the same shapes as in a double caterad but without any compositions there either. There should be monads on this category whose algebras are (1) double categories, (2) augmented double categories, in which pinwheels etc. can be composed, (3) double caterads, (4) augmented double caterads, (5) doubly-weak double categories, and (6) augmented doubly-weak double categories.
Aaron David Fairbanks (Sep 29 2022 at 20:29):Thank you Mike, that is very helpful. I will from now on start calling these "double caterads" in my head.
Mike Shulman (Sep 29 2022 at 20:31):The notions of doubly-weak double category that have been suggested elsewhere then arise by restricting the shapes that you allow in the double computads. Verity's [[double bicategories]] have just squares and bigons, while the "cubical bicategories" once proposed by Garner have only squares.
Jacques Carette (Sep 30 2022 at 12:02):And now I know why I got stuck trying to work out double categories in Agda (its MLTT core, not cubical) has been so hard: strict anything is really hard, it's 'simplest' to always work with weak structures. Didn't know that trying to do doubly-weak double categories might turn out to be 'new'.
Nathanael Arkor (Sep 30 2022 at 13:59):Jacques Carette said:
And now I know why I got stuck trying to work out double categories in Agda (its MLTT core, not cubical) has been so hard: strict anything is really hard, it's 'simplest' to always work with weak structures. Didn't know that trying to do doubly-weak double categories might turn out to be 'new'.
Just to clarify, "weak" in this context is being used to mean nonrepresentable/"virtual", rather than "pseudo". Double categories that have composition in both directions, but associative/unital only up to isomorphism have been studied in the literature before, under the name [[double bicategories]].
Jacques Carette (Sep 30 2022 at 14:52):Ah, thank you, I had misunderstood. And I had not idea that [[double bicategories]] was were I ought to look, as that's not the expected name (as the page acknowledges). But now I know, that should help.
Mike Shulman (Sep 30 2022 at 16:47):@Nathanael Arkor, I don't think that's right. At least, that's certainly not what I meant by "weak" -- I meant it in the sense of "pseudo". And I'm pretty sure Aaron meant "pseudo" too, because he asked "Are doubly weak double categories equivalent to [double caterads] that are both vertically and horizontally representable?"
Mike Shulman (Sep 30 2022 at 16:49):Verity's double bicategories are a notion of "doubly-weak double category", but they're a little odd because they have bigons as separate data in addition to the squares, and in particular a double bicategory in which all the coherences are identities is more general than a strict double category in the traditional sense. One of the virtues of the double-caterad approach to doubly-weak double categories is that it avoids this issue.
Nathanael Arkor (Sep 30 2022 at 17:48):@Mike Shulman: ah, sorry, I misunderstood – thanks for the clarification. When you wrote
Regarding double categories, this is actually something I spent a while thinking about!
I thought you meant the "X"s that Aaron mentioned, rather than the representable kind (because your next message was about the nonrepresentable kind, and I thought it was talking about the same structure). Sorry for the confusion @Jacques Carette!
Mike Shulman (Sep 30 2022 at 17:52):I meant both! (-:
Jacques Carette (Oct 01 2022 at 08:32):So now I am indeed confused. What is a good definition of "doubly weak double category" in the pseudo sense that I should be using, as a means to formalize that in Agda?
John Baez (Oct 01 2022 at 16:31):Probably Mike Shulman's definition. But you will have to extract it from him:
Regarding double categories, this is actually something I spent a while thinking about! In fact, I have a half-written paper lying around waiting to be completed (or superseded). This definition of doubly-weak double category isn't in the literature, so far as I know, but I believe it's the best one.
Jacques Carette (Oct 01 2022 at 21:46):Perhaps I should try summoning @Mike Shulman and that might work?
Mike Shulman (Oct 02 2022 at 00:09):I don't have it written down in explicit form. My half-written notes define them as algebras for a monad on the category of double computads, but the monad isn't very explicit. The definition is basically you have composition and unit operations on both sets of arrows, with no axioms, and then a set of squares with any possible sequences of composable arrows on all four boundaries, with "all the possible composition operations" of those.
Mike Shulman (Oct 02 2022 at 00:09):I don't even know whether there is a finite presentation of that definition.
Mike Shulman (Oct 02 2022 at 00:10):I think it should be possible to give an equivalent definition by starting with a [[double bicategory]] and then imposing as an extra axiom that the canonical maps from bigons to degenerate squares are bijections.
Mike Shulman (Oct 02 2022 at 00:10):That might be easiest for formalization.
Jacques Carette (Oct 03 2022 at 07:32):Thanks - I'll give that a try.