Category Theory
Zulip Server
Archive

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.

Stream: learning: questions

Topic: Coherence for graphical languages

Alexander Cowtan (Jan 19 2021 at 07:44):

Hi all, I'm new. Aiming to challenge the "No question is dumb" mantra as much as possible.

In "A survey of graphical languages for monoidal categories" by Selinger, it says for many kinds of monoidal categories with extra structure (e.g. pivotal categories, braided autonomous categories) that coherence of the graphical language has only been proved for special cases, such as for diagrams over a simple signature.

Has coherence since been proven in the general case for such categories since then? I am particularly interested in the cases of braided pivotal categories & tortile (ribbon) categories.

John Baez (Jan 19 2021 at 08:04):

Hi! Whew, you're going to have to work a lot harder if you're trying to ask a dumb question.

Maybe @Cole Comfort might know about coherence theorems for braided pivotal categories or ribbon categories. I don't. I would be inclined to just google it!

Jules Hedges (Jan 19 2021 at 12:13):

I don't know about pivotal & ribbon categories, but I think this paper https://arxiv.org/abs/1508.01069 ("String diagrams for traced and compact categories are oriented 1-cobordisms") fills in the missing cases from Selinger for, as it says, traced and compact closed categories

Cole Comfort (Jan 19 2021 at 18:19):

John Baez said:

Hi! Whew, you're going to have to work a lot harder if you're trying to ask a dumb question.

Maybe Cole Comfort might know about coherence theorems for braided pivotal categories or ribbon categories. I don't. I would be inclined to just google it!

I am not aware of any such coherence theorems. I think that everyone just assumes that the "obvious" coherence conditions are complete so there probably wouldn't be too much of a reward in actually proving them.
Maybe @Antonin Delpeuch has more insight into such things.

Antonin Delpeuch (Jan 19 2021 at 20:30):

Yes, can we have more people proving these things? :) And perhaps let's stop calling them coherence theorems since it creates a really annoying clash with the "all diagrams commute" sort of result. Soundness and completeness, anyone?

Amar Hadzihasanovic (Jan 19 2021 at 21:12):

Antonin Delpeuch said:

Yes, can we have more people proving these things? :) And perhaps let's stop calling them coherence theorems since it creates a really annoying clash with the "all diagrams commute" sort of result. Soundness and completeness, anyone?

Yes please! I've been saying this for ages.

Amar Hadzihasanovic (Jan 19 2021 at 21:13):

“Adequacy” also exists as a term for soundness+completeness if people prefer a single word.

Amar Hadzihasanovic (Jan 19 2021 at 21:22):

Actually I already complained about this here...

Antonin Delpeuch (Jan 20 2021 at 07:21):

Yay for "adequacy"!

Alexander Cowtan (Jan 20 2021 at 08:15):

Thanks all.

John Baez said:

Hi! Whew, you're going to have to work a lot harder if you're trying to ask a dumb question.

I'll try my best.

Jules Hedges (Jan 20 2021 at 11:05):

History question: Does anyone know who to blame for the terminology "coherence" for things related to graphical languages? Is it Peter Selinger, or was someone using it earlier?

Fawzi Hreiki (Jan 20 2021 at 11:55):

Well there’s this book from the 70s all about coherence questions where Mac Lane originally proved the coherence theorem for monoidal categories

Fawzi Hreiki (Jan 20 2021 at 11:56):

But I’m not sure if that’s what you mean regarding graphical languages

Jules Hedges (Jan 20 2021 at 11:57):

Nope, I mean results like "the free blah category on a signature is isomorphic to the category whose morphisms are blah diagrams modulo blah topological moves"

Jules Hedges (Jan 20 2021 at 11:58):

The issue being that those results are only loosely related to Mac Lane style "all diagrams commute" results, and Mac Lane got there first

Amar Hadzihasanovic (Jan 20 2021 at 12:50):

I don't know if Selinger invented this use of coherence, but they did probably popularise it.

I think it stems from a misreading of what Mac Lane's use of “coherence” refers to. I imagine that Selinger or their source interpret Mac Lane's theorem as something like
The equational theory of monoidal categories is sound and complete for... our ideal model of what a monoidal category should be,
which is the one in which all well-formed diagrams made up of structural morphisms commute.
So a soundness-and-completeness result with respect to the coherent model as an embodiment of an ideal model that we aspire to.

And then you get the graphical language theorems as generalisations of this reading, where now our “ideal model” is the one expressed by the string diagram picture.

The misreading is that “coherence” refers to a property of the equational theory, that is, that Mac Lane's theorem is
The equational theory of monoidal categories is “coherent” for the model in which all diagrams commute.
Whereas coherence is a property of the free models, that is, Mac Lane's theorem is
The free models of the equational theory of monoidal categories are coherent.

Amar Hadzihasanovic (Jan 20 2021 at 13:00):

It's a bit like thinking that Gödel's incompleteness theorem is not the statement that
Peano arithmetic is incomplete
but the statement that
The natural numbers are incomplete...

Mike Shulman (Jan 20 2021 at 16:02):

I don't understand the hairs that are being split here. Set aside the question of whether "all diagrams commute", since as is well known there are plenty of "coherent" structures in which not all diagrams commute. A more generalizable way to state MacLane's result is that it gives a method for determining whether a particular diagram shape in the language of monoidal categories commutes in general. This is equivalent to giving a concrete description of free monoidal categories. String diagrams can also be interpreted as doing both of these things.

Mike Shulman (Jan 20 2021 at 16:03):

(A more problematic usage, in my opinion, is saying "coherence theorem" for a result of the form "every pseudo-blah is equivalent to a strict blah". This is not completely unrelated, but certainly not equivalent, since there are plenty of coherence theorems that do not imply a full strictification theorem.)

Amar Hadzihasanovic (Jan 20 2021 at 16:27):

I agree with your version of generalised Mac Lane coherence -- I didn't mean to say that all coherence results are of the form "all diagrams commute", but they are of the form "these particular diagrams commute" or better in some contexts "commute up to a higher cell"... That's certainly also the usage of coherence by French rewriting theorists :)

Amar Hadzihasanovic (Jan 20 2021 at 16:29):

On the other hand I don't think I agree that "string diagrams can be interpreted as doing these things". My reading of Joyal-Street is that it is, by itself, a theorem on strict monoidal categories, that only says something about general monoidal categories because of Mac Lane's coherence theorem; but the two parts are logically independent.

Amar Hadzihasanovic (Jan 20 2021 at 16:34):

Specifically, it is coherence which gives a "pasting theorem" allowing to interpret string diagrams in arbitrary monoidal categories by choosing a bracketing on the sources and targets of individual boxes/nodes. This only "coherently" extends to composite diagrams because coherence ensures that rebracketing can be done in a unique way to compose things together.

Amar Hadzihasanovic (Jan 20 2021 at 16:35):

I agree that strictification is another related, but not equal notion to either of the ones we're discussing.

John Baez (Jan 20 2021 at 19:25):

I think of Selinger's use of the word "coherent" as a natural outgrowth of Mac Lane's coherence theorem. Mac Lane used the word "coherent" in the main theorem of his 1963 paper Natural associativity and commutativity. Maybe the applications to graphical languages is a bit different,... but I doubt Selinger thought he was doing anything new in using the word that way.

Amar Hadzihasanovic (Jan 20 2021 at 20:27):

@John Baez Yes, Mac Lane says:

Coherence can also be defined in terms of diagrams: it requires that any diagram with vertices iterates of $\otimes$ and edges expansions of instances of $a$ be commutative.

So a property that “certain diagrams commute in all models”. It's a property of models of a theory.
It's analogous, for example, to the property that all models of the theory of vector spaces are free models.
That's very different from soundness+completeness, which is a property of a theory with respect to a class of models, and which is what Selinger's theorems are about. I really don't think there's any “hair splitting” involved.

Amar Hadzihasanovic (Jan 20 2021 at 20:30):

If you had a theorem stating roughly
“These axioms are sound and complete for vector spaces over a field $k$. Also, (Freeness theorem): all models of this theory are free.”
And then somebody wrote a survey of soundness+completeness theorems calling them “freeness theorems”, I don't think there would be any doubt that it's a bad choice.

Nathanael Arkor (Jan 20 2021 at 20:36):

Amar Hadzihasanovic said:

“Adequacy” also exists as a term for soundness+completeness if people prefer a single word.

Unfortunately, it's also used in denotational semantics to mean something else. (A lot of the terminology in denotational semantics is bad, though.)

Amar Hadzihasanovic (Jan 20 2021 at 20:39):

Comploundness...

Amar Hadzihasanovic (Jan 20 2021 at 20:41):

Still a better word than “clopen”!

Mike Shulman (Jan 21 2021 at 16:32):

I don't see why one can't talk about a coherence theorem for strict structures, in the sense of a concrete description of the free such structure. It's not the same theorem as a coherence theorem for weak structures, but if it's doing the same thing for the relevant 2-monad we should be able to call it the same thing.

Mike Shulman (Jan 21 2021 at 16:35):

Amar Hadzihasanovic said:

So a property that “certain diagrams commute in all models”. It's a property of models of a theory.

You could say that, but you could also regard soundness+completeness as a property of models. Soundness means that something provable in the theory is true in all models, and completeness means that something not provable in the theory is false in some model. I think "certain diagrams commute in all models" is much more closely analogous to (and, given the right framework, even an instance of) "something provable in the theory is true in all models" than it is to something like "all models are free".

Amar Hadzihasanovic (Jan 21 2021 at 19:39):

Yes, I see what you are saying. Still, my feeling is that there are two logically independent parts to something like Joyal and Street's result. There is what I would call properly coherence theorems, which can be put in the form
The universal morphisms from the free models of this theory to the free models of this stricter theory are (weak) equivalences,
and then there are “coherence theorems” in Selinger's sense which are of the form
Free models of the stricter theory have this concrete description up to isomorphism.
In the paradigmatic example, Mac Lane proves that the quotient functor from free monoidal categories to free strict monoidal categories is an equivalence, and then Joyal & Street prove that free strict monoidal categories can be presented by string diagrams up to ambient isotopy. I don't see any logical dependency between the two.
And my impression is that even Joyal & Street use “coherence” to refer to the first property, even though the two can be somewhat conflated into a single statement, like “free models of this theory are weakly equivalent to these concrete, stricter models”.

Amar Hadzihasanovic (Jan 21 2021 at 19:44):

I still think that the analogy with “vector spaces are free models” is not off the mark. You can state two logically independent theorems:
All vector spaces are isomorphic to free vector spaces
and
The free vector space on a set is the vector space of formal linear combinations of elements of the set.
I would say that Mac Lane's coherence theorem is logically analogous to the first and Selinger's coherence theorems are analogous to the second.

Mike Shulman (Jan 25 2021 at 02:05):

Yes, certainly the result decomposes in that way. But I don't see why you would insist that only one half of it should be called a "coherence theorem". In fact the part of it that you want to call a "coherence theorem" seems to me less like a coherence theorem than the other part, because it doesn't give a concrete description of anything; it only says that one abstract thing is equivalent/isomorphic to some other abstract thing. Rather than a coherence theorem, I'd be tempted to call it more of a strictification theorem for free structures.

Amar Hadzihasanovic (Jan 25 2021 at 07:16):

I think that Mac Lane uses the word “coherence” in the sense of “all the choices that we make are coherent/consistent” because all a priori different parallel paths of morphisms are actually equal. In more homotopical settings you could say “we have a contractible space of choices”. To me this reading makes sense based on the non-mathematical semantics of the word. With strict structures there is a unique choice so “coherence” is trivial, not something that deserves a coherence theorem.
It is also this meaning of the word that French rewriting theorists have in mind in the theory of “coherent presentations”, so maybe I'm biased because I'm interested in this.
How do you relate the (non-mathematical) meaning of “coherence” to “being a concrete description of something”?

Amar Hadzihasanovic (Jan 25 2021 at 07:22):

“Strictification for free structures” to me is just a way to encapsulate coherence in the fact that, roughly “quotienting out the spaces of choices produces an acyclic fibration”, and that's the comparison map between a free model and a free strict model.

Mike Shulman (Jan 25 2021 at 13:28):

I'm getting kind of bored of this conversation, but I'll give it one more go. Yes, the original meaning of coherence derived from "all the choices are consistent", but I think that was because the first coherence theorems were of the "all diagrams commute" kind. When you generalize beyond that, I suppose one might argue that the word "coherence" shouldn't apply (which would exclude it from being used, for instance, for any kind of "coherence theorem" for braided monoidal categories), but I think that ship has sailed. Nowadays we certainly apply "coherence theorem" to situations in which not all diagrams commute, and in that case what it means is giving a concrete presentation.

Jules Hedges (Jan 25 2021 at 13:42):

I'm kind of interested in this conversation just because I've never encountered anyone actively defending the status quo terminology before, I've only ever seen people who are actively against it and people who don't care

Amar Hadzihasanovic (Jan 25 2021 at 14:32):

I'm no prescriptivist and I don't mind if there's conflicting terminology. The only moments when I care is when I meet someone learning string diagrams and monoidal categories, and they invariably get confused about what the hell coherence is. But we'll have to disagree.
I never said that coherence is necessarily “all diagrams commute”, rather it's about “some diagrams commute” (maybe up to a higher cell). That covers the usage of “coherence” in most 'classical' papers that I can think of: Mac Lane, Kelly-Laplaza, Joyal-Street, Gordon-Power-Street... Also perhaps the one where I found it spelled out most clearly, “coherence for weak units” by Joyal and Joachim Kock where the coherence theorem is explicitly of the form “a certain 2-category is contractible”. Honestly I think Selinger is the exception and the only “major” paper which in my opinion misuses the word coherence. So I don't think it's fair to put it like “It's a done deal, everyone uses coherence this way nowadays”.

Todd Trimble (Jan 25 2021 at 15:02):

My thesis was on coherence theorems, and I understand the term the same way as Mike. A coherence theorem gives a way to decide equality in free categorical structures. This usage has been with us a long time, and was codified by Australian category theorists in the early 70's.

Amar Hadzihasanovic (Jan 25 2021 at 15:46):

(Sorry, I wrote then deleted a few messages because I think I misunderstood what you meant by “decide equality” the first time -- I interpreted it in the sense of a computational decision procedure, but now I think you meant “define equality”, i.e. give a complete presentation of a theory of equality)

Amar Hadzihasanovic (Jan 25 2021 at 15:52):

I think maybe it's starting to click to me why we are not understanding each other :grinning:

Amar Hadzihasanovic (Jan 25 2021 at 15:55):

For you and Mike, a free model is defined by a universal property, as the image of a left adjoint to a forgetful functor from the category of models -- is that right?

While all this time I've been thinking “as a computer scientist”: a free model for me is a syntactic model of a certain presented theory.

Amar Hadzihasanovic (Jan 25 2021 at 15:56):

That's why it didn't make sense to me. I'm thinking of coherence as a property of a presented theory which is equivalently a property of its syntactic models.

Fawzi Hreiki (Jan 25 2021 at 15:56):

Ah but then you're distinguishing syntactic presentations which give rise to the same object right?

Amar Hadzihasanovic (Jan 25 2021 at 15:58):

Yes! So for me a coherence theorem is literally the fact that certain diagrams made from the generators of this presentation commute up to equations or higher-dim generators of this presentation.
Which certainly can give a procedure for deciding equality in free structures (so Todd's definition makes sense to me as a consequence of coherence).

Fawzi Hreiki (Jan 25 2021 at 15:59):

The most basic coherence theorem we learn is that the operation in a group is associative. This means that when writing down a group presentation, we can do so without brackets. The words in a group are akin to the diagrams in a category (they're both just generalised elements). Just because we can present the same element in a group in different ways (i.e. via different words), it doesn't mean we don't have coherence.

Amar Hadzihasanovic (Jan 25 2021 at 16:00):

While for Todd and Mike, if now I understand correctly, a coherence theorem is a theorem which constructs a presentation for a 'free model' which is defined 'semantically' by a universal property.

Amar Hadzihasanovic (Jan 25 2021 at 16:01):

So of course we could not understand each other, we were thinking of different meanings of “free model”.

Fawzi Hreiki (Jan 25 2021 at 16:02):

So is your understanding of 'free model' a syntactic presentation?

Amar Hadzihasanovic (Jan 25 2021 at 16:03):

Yeah, I guess for me a “free monoidal category” is a syntactic model made up of building blocks that are associators, unitors, etc...

Amar Hadzihasanovic (Jan 25 2021 at 16:05):

In fact I should have known better, because I conflated “theory” with “presentation of a theory” a few times.

Fawzi Hreiki (Jan 25 2021 at 16:05):

For me, a pretty important lesson from category theory is to distinguish between presentations and their universal realisations.

Amar Hadzihasanovic (Jan 25 2021 at 16:06):

Yep. So the thing is, I would still say that Mac Lane's coherence theorem is about a presentation of the theory of monoidal categories.

Amar Hadzihasanovic (Jan 25 2021 at 16:07):

Or equivalently about its free models in the sense of syntactic models.

Amar Hadzihasanovic (Jan 25 2021 at 16:08):

But I think I'm starting to understand better how the term has shifted in usage.

Jules Hedges (Jan 25 2021 at 16:11):

Am I understanding right? A general coherence theorem says "the free [as in universal property] foo is equivalent to bar [defined concretely]"; results of the form "all diagrams commute [except those that don't]" can be seen as a special case of that?

Amar Hadzihasanovic (Jan 25 2021 at 16:12):

I think it may be something like:
Mac Lane: “Coherence theorem: this presentation of the theory is coherent, that is, the syntactic models are coherent.”

-> (first shift): “Coherence theorem: the free models of this theory are equivalent to these syntactic models, which are coherent.”

-> (second shift): “Coherence theorem: the free models of this theory are equivalent to these syntactic models.”

Amar Hadzihasanovic (Jan 25 2021 at 16:13):

And then finally Selinger's usage of “Coherence theorem: the free models of this theory are equivalent to these concrete models.”

Jules Hedges (Jan 25 2021 at 16:15):

My personal understanding of the word "syntactic" has expanded to include diagrams, as in "diagrams are 2-dimensional syntax whereas strings and terms are 1-dimensional syntax"

Amar Hadzihasanovic (Jan 25 2021 at 16:16):

While I agree for some formalisations of string diagrams, I cannot really agree for “embedded real manifolds modulo ambient isotopy”.

Jules Hedges (Jan 25 2021 at 16:22):

The usual coherence theorem for monoids is "the free monoid on a set is equivalent to the monoid of strings with concatenation". A less useful but equally valid one is "the free monoid on a set is equivalent to a bunch of labelled points on a line, modulo isotopy"

Amar Hadzihasanovic (Jan 25 2021 at 16:25):

Well, you see, for me a coherence theorem for monoids would be “all well-formed binary bracketings of the same string are equal”.

Nathanael Arkor (Jan 25 2021 at 16:25):

Isn't that the same statement?

Amar Hadzihasanovic (Jan 25 2021 at 16:27):

No, my statement refers to the syntactic model for the presentation of monoids with a binary multiplication. That's where binary bracketings come from.

John Baez (Jan 25 2021 at 16:27):

Not the same, merely equivalent. :upside_down:

Nathanael Arkor (Jan 25 2021 at 16:28):

Right. The free monoid is the one with binary bracketings. Asserting it's equal to the monoid of strings is the same as saying that all bracketings are equal.

Nathanael Arkor (Jan 25 2021 at 16:28):

To what extent would it be reasonable to say that coherence theorems are results stating that free $\Sigma$-algebras are equivalent to $\Sigma'$-algebras, where $\Sigma$ and $\Sigma'$ are presentations and $\Sigma'$ is a "simpler" presentation?

Nathanael Arkor (Jan 25 2021 at 16:28):

The coherence theorem for monoids is then "free monoids are equivalent to lists".

Amar Hadzihasanovic (Jan 25 2021 at 16:29):

Nathanael Arkor said:

Right. The free monoid is the one with binary bracketings. Asserting it's equal to the monoid of strings is the same as saying that all bracketings are equal.

You are making the same “mistake” that I was making! Thinking that free model = syntactic model. That's CS-thinking.

Nathanael Arkor (Jan 25 2021 at 16:29):

I think it's a tautology to say that the free model is the syntactic model.

Amar Hadzihasanovic (Jan 25 2021 at 16:29):

For Mike and Todd a free model is one that's obtained through the left adjoint of the forgetful functor from monoids to sets.

Nathanael Arkor (Jan 25 2021 at 16:30):

There has to be a syntactic presentation by definition, though. It just might not be the one you want.

Amar Hadzihasanovic (Jan 25 2021 at 16:30):

Or through “a” left adjoint. Really it refers to a whole (contractible) groupoid of things.

Amar Hadzihasanovic (Jan 25 2021 at 16:30):

(Because all left adjoints are uniquely naturally isomorphic as functors.)

Jules Hedges (Jan 25 2021 at 16:31):

To muddy the waters further: A syntactic monoid is (in my opinion) literally defined in terms of trees. Proving that it's equivalent to strings over the same set together with the extra symbols "(" and ")", satisfying a certain balance property, is an exercise you can give to make 1st years suffer

John Baez (Jan 25 2021 at 16:31):

The free monoid is the one with binary bracketings.

It depends on what you mean by "the free monoid". You could argue it's the one freely formed by a binary operation mod the equivalence relation (ab)c = a(bc) (and some laws involving units), and then we get the binary bracketings you're talking about. But you could also argue it's the monoid of strings on the generators. Since they're isomorphic, they're both perfectly fine "free monoids" on a given set.

John Baez (Jan 25 2021 at 16:32):

But proving they're isomorphic is a kind of "coherence theorem".

Amar Hadzihasanovic (Jan 25 2021 at 16:35):

So can we agree that these are the two competing reading of coherence?

• Coherence as a property of a presented theory, or equivalently, of its syntactic models; namely, that certain diagrams made of generators commute up to higher generators or relations.
• Coherence as a property of the free models of a theory, where being free is defined wrt to a free-forgetful adjunction for the category of models; namely, that they are equivalent to the syntactic models of a certain presentation.

John Baez (Jan 25 2021 at 16:36):

By the way, I think there are lots of interesting questions here, and to me the least interesting questions are "what is coherence?" and "what are coherence theorems?", since those are purely about definitions.

John Baez (Jan 25 2021 at 16:39):

The two competing readings of coherence sound a bit like this to me:

• proving that a syntactic model of a presented theory is equivalent to a free model of that theory;
• proving that a free model of a theory is equivalent to a syntactic model of a presentation of that theory.

John Baez (Jan 25 2021 at 16:40):

I'm sort of joking... one of your two choices involved diagrams commuting... but they don't sound so different to me.

Amar Hadzihasanovic (Jan 25 2021 at 16:41):

Yeah, it's more like:

• the theorem is that a specific presentation has a property.
• the theorem is that a theory has a specific presentation.

Fawzi Hreiki (Jan 25 2021 at 16:42):

I think the difficulty here is that most of the time, when we define a notion of syntactic presentation, we do so quite informally and without defining what the category of presentations looks like.

Amar Hadzihasanovic (Jan 25 2021 at 16:42):

The confusion is also the sometimes they are put together into

• the theorem is that a theory has a specific presentation which has a property.

Nathanael Arkor (Jan 25 2021 at 16:42):

Both of these seem like they can be reduced to "one specific presentation is equivalent to another specific presentation".

Nathanael Arkor (Jan 25 2021 at 16:42):

E.g. the presentation of monoidal categories is equivalent to the presentation of strict monoidal categories.

Amar Hadzihasanovic (Jan 25 2021 at 16:46):

John Baez said:

By the way, I think there are lots of interesting questions here, and to me the least interesting questions are "what is coherence?" and "what are coherence theorems?", since those are purely about definitions.

I think that there is a lot to learn from the fact that the same word means related but different things to two of us, and trying to understand where the difference comes from.

Fawzi Hreiki (Jan 25 2021 at 16:47):

I think the nlab definition of coherence in terms of contractibility of the space of choices is pretty intuitive. The idea is that we may have many different options, but in the end it shouldn't really matter which one we choose. This relates to syntax and diagrams I think in the following way: supposing we follow certain rules regarding how we build our syntactic presentations, we will stay within this contractible space of choices.

Fawzi Hreiki (Jan 25 2021 at 16:48):

Its analogous to a soundness result in logic: supposing we start with a presentation and follow the deduction rules of the ambient language, we will always stay within the space of things true in the free model on that presentation.

Amar Hadzihasanovic (Jan 25 2021 at 16:50):

Fawzi Hreiki said:

I think the nlab definition of coherence in terms of contractibility of the space of choices is pretty intuitive. The idea is that we may have many different options, but in the end it shouldn't really matter which one we choose. This relates to syntax and diagrams I think in the following way: supposing we follow certain rules regarding how we build our syntactic presentations, we will stay within this contractible space of choices.

Oh, that's the nLab definition? I used those same words a few messages ago, but I must have forgotten where they came from :grinning_face_with_smiling_eyes:

Fawzi Hreiki (Jan 25 2021 at 16:50):

The contractibility 'definition' is from the nlab: https://ncatlab.org/nlab/show/coherence+law

Amar Hadzihasanovic (Jan 25 2021 at 16:52):

Yes, that's certainly where I got my own idea from, then. That's certainly coherence in the first sense (property of a presentation), because the choices are relative to specific generators/structural cells.

John Baez (Jan 25 2021 at 16:53):

Amar Hadzihasanovic said:

John Baez said:

By the way, I think there are lots of interesting questions here, and to me the least interesting questions are "what is coherence?" and "what are coherence theorems?", since those are purely about definitions.

I think that there is a lot to learn from the fact that the same word means related but different things to two of us, and trying to understand where the difference comes from.

Yes. I was just saying that I don't care which definition of "coherence" or "coherence theorem" is "correct". The interesting part is sorting out various concepts and their relationships. Maybe this remark of mine was too obvious to be necessary.

Nathanael Arkor (Jan 25 2021 at 16:58):

I think it is a useful remark to make, because I think for some people two concepts are obviously the same, so they're happy to conflate those concepts; whereas for others, it's not clear, especially because as-stated the two concepts look different. E.g. if you take the 6 different ways to describe the coherence theorem(s) for monoidal categories on the nLab page, it's not immediately clear why some imply the others (and if these statements would generalise to other situations).

Nathanael Arkor (Jan 25 2021 at 16:59):

If they do always generalise, then it makes it more obvious that "coherence" has a single meaning, but may be phrased differently, but if they don't always generalise, then it's important to draw the distinction.

Nathanael Arkor (Jan 25 2021 at 17:00):

It would be nice to have a paper proving coherence in various ways for some reasonably general notion of presentation/theory and showing them to be equivalent (or at least related). (Though this is essentially what @John Baez said already.)

Jules Hedges (Jan 25 2021 at 17:02):

It's not totally unreasonable to want different names for these closely related but subtly different things. There's a tension between "equivalent things should have the same name" and "equivalent but not identical things should have different names"

John Baez (Jan 25 2021 at 17:03):

I can imagine a very nice paper going through all 6 theorems about monoidal categories on the nLab, proving them, and discussing how they're related to each other - e.g. how you can prove some starting from others.

(Nathanael mentioned 7 but I just see 6.)

On the other hand, monoidal categories are a bit "too easy"; symmetric monoidal categories introduce important new challenges since for these the "all diagrams commute" formulation fails if interpreted naively.

Nathanael Arkor (Jan 25 2021 at 17:05):

Jules Hedges said:

It's not totally unreasonable to want different names for these closely related but subtly different things. There's a tension between "equivalent things should have the same name" and "equivalent but not identical things should have different names"

That's also true, and such a paper would be well-placed to give proper names to each of approaches.

Nathanael Arkor (Jan 25 2021 at 17:06):

(Nathanael mentioned 7 but I just see 6.)

Just a typo!

John Baez (Jan 25 2021 at 17:07):

Whew, I thought this was another case of not agreeing whether two theorems are the same.

Fawzi Hreiki (Jan 25 2021 at 17:07):

I think the word 'coherence' is like 'space' or 'structure'. It doesn't really need a single rigid definition so long as all the different uses somehow cohere (sorry for the pun).

Nathanael Arkor (Jan 25 2021 at 17:07):

I think Gould's Coherence for Categorified Operadic Theories could be a good starting point.

Nathanael Arkor (Jan 25 2021 at 17:09):

(This generalises the "Every monoidal category is monoidally equivalent to a strict monoidal category." version of coherence.)

Amar Hadzihasanovic (Jan 25 2021 at 17:25):

I read Gould and for a second I thought it was the other thread on Bach.

Todd Trimble (Jan 25 2021 at 21:47):

Amar Hadzihasanovic said:

(Sorry, I wrote then deleted a few messages because I think I misunderstood what you meant by “decide equality” the first time -- I interpreted it in the sense of a computational decision procedure, but now I think you meant “define equality”, i.e. give a complete presentation of a theory of equality)

No, I actually meant what I said. To solve a coherence problem means to give a method for deciding when two morphisms in the free structure are equivalent.

Amar Hadzihasanovic (Jan 25 2021 at 21:57):

Todd Trimble said:

No, I actually meant what I said. To solve a coherence problem means to give a method for deciding when two morphisms in the free structure are equivalent.

So is Joyal-Street's theorem about string diagrams a coherence theorem in your opinion? It presents free strict monoidal categories in terms of equivalence classes modulo isotopy of real manifolds, which seems quite undecidable.

Amar Hadzihasanovic (Jan 25 2021 at 21:59):

In general these coherence theorems for graphical languages that are being debated do not strike me as results that give algorithmic decision procedures.

Amar Hadzihasanovic (Jan 25 2021 at 22:24):

I'm starting to think that maybe your definition of coherence is even more restrictive than mine?

I think the positions are:

• Mike: to solve a coherence problem is to give a presentation of the free model of a theory.
• Me: to solve a coherence problem is to characterise what morphisms are equal in a syntactic model of a theory (wrt a presentation).
• Todd: to solve a coherence problem is to give a decision procedure for equality of morphisms in a syntactic model of a theory (wrt a presentation).

Do you accept this characterisation?

If so, than a solution of the coherence problem in your sense is stronger than a solution in my sense and definitely much stronger than in Mike's sense...

Todd Trimble (Jan 25 2021 at 22:26):

Right, it would not be a coherence theorem in the sense I indicated. String diagrams give a way of presenting free categorical structures in particularly useful geometric form.

What I said in my previous post is not exactly what Mike said, but then again, in my previous post, instead of trying to say what a coherence theorem is, I shifted over to say how I understand what it means to solve a coherence problem. I'm willing to agree there could be a useful distinction.

Todd Trimble (Jan 25 2021 at 22:29):

(I haven't read through the entire thread, so I'm not immediately sure what your position means.)

Amar Hadzihasanovic (Jan 25 2021 at 22:37):

Uhm, I suppose for me coherence is “these diagrams commute” without necessarily being translated into a decision procedure. For example I would be happy with a coherence theorem that assigns to morphisms $f$ elements $m(f)$ of a monoid whose word problem is undecidable, and says that “$f = g$ if and only if $m(f) = m(g)$”.

Amar Hadzihasanovic (Jan 25 2021 at 22:37):

But that is a minor distinction.

Todd Trimble (Jan 25 2021 at 22:47):

So where "I agree with Mike" was where he said "that ship has sailed" (coherence no longer means all diagrams commute) and where he said (Jan. 20) "A more generalizable way to state MacLane's result is that it gives a method for determining whether a particular diagram shape in the language of monoidal categories commutes in general." I was giving a strong sense to "determining". A really strong desideratum for solving a coherence problem would be in the form of a strongly normalizing confluent rewrite system on syntactic expressions so that the normal forms are in bijection with the morphisms in the free structures.

Amar Hadzihasanovic (Jan 25 2021 at 22:52):

Great, I also agree with Mike (and you) on both of those :smile: In fact I had already agreed on Jan 20!
Then I had disagreed when he added “String diagrams can also be interpreted as doing both those things” because I don't think string diagrams say anything about associators or unitors, which are also part of the language of monoidal categories.

Todd Trimble (Jan 25 2021 at 22:53):

Of course, there are also lots of distinctions that could be made. For example, Kelly and Mac Lane in their paper Coherence in Closed Categories give what I would call a partial coherence theorem, in which it's possible to decide equality of morphisms between objects belonging to a restricted class (roughly, objects which don't "essentially" involve the monoidal unit -- I can be more precise if need be).

Amar Hadzihasanovic (Jan 25 2021 at 22:55):

Or rather, that's poorly worded. They don't say anything by themselves in addition to Mac Lane's coherence theorem. As in, you can give a statement of coherence which is of the form “these morphisms are equal if their interpretation in string diagrams is equal modulo ambient isotopy”. But really that's Mac Lane (equal if equal in the free strict model) + Joyal-Street (equal in the free strict model if equal as string diagrams).

Todd Trimble (Jan 25 2021 at 22:56):

I'm not so fussed about the associators and units, because already in Geometry of Tensor Calculus, they re-present the classical Mac Lane coherence theory (in terms of ana-objects or "cliques") as a preamble to their string diagram calculus, which refers to symmetric strict monoidal categories, etc. (written while you were writing your last comment; I'm a slow typist).

Amar Hadzihasanovic (Jan 25 2021 at 22:57):

And really that was the whole beginning of this “debate”... whether it makes sense to call both of these two sides “coherence theorems”, or are they one coherence theorem + one soundness&completeness theorem.

Todd Trimble (Jan 25 2021 at 22:58):

Yeah, I don't know, I've probably been "guilty" in the past of referring to the Joyal-Street theorem as a "coherence theorem", while forgetting the sense of coherence theorem that I learned from reading the classical 70's stuff, e.g., in Lecture Notes in Math. 420.

Todd Trimble (Jan 25 2021 at 23:01):

You may know of even earlier work by Lambek and his school (e.g., Szabo) which presented morphisms in free structures as equivalence classes of sequent deductions. That's a different style of syntactic presentation (but a breakthrough, in that techniques of cut elimination were imported).

Amar Hadzihasanovic (Jan 25 2021 at 23:03):

I've seen it mentioned (maybe in your article on linearly distributive cats?) but so far I've found it too scary to read directly...

Todd Trimble (Jan 25 2021 at 23:06):

So what happens there is that while a free monoidal closed category on a set, say, is presented by saying that a morphism "is" a suitable equivalence class of sequent deductions, the beauty is that by passing to cut-free deductions, all these equivalence classes are finite sets -- and thus equality can be decided by checking whether any old cut-free sequent presentation of morphism $f$ lies in the same finite class as one for another morphism $g$. That in principle does give a solution to the coherence problem in my sense, since one just enumerates the finitely many possibilities.

Todd Trimble (Jan 25 2021 at 23:09):

(It's not a super-elegant solution, necessarily, but it is a solution. The real challenge is to turn it into something humanly elegant.)

Todd Trimble (Jan 25 2021 at 23:12):

Now it may be possible to give an actual decision procedure for things like the free symmetric monoidal category generated by a tensor scheme. To be honest, I've been out of the game for quite some time, so I don't know what literature might be out there on this sort of thing. It's sort of in a different direction to the spirit of Joyal-Street.

Amar Hadzihasanovic (Jan 25 2021 at 23:15):

I see. I guess that can reach free non-algebraic structures, like things where there are free witnesses of existential statements? That seems outside the scope of the usual coherence theorems.

Todd Trimble (Jan 25 2021 at 23:19):

Well, perhaps, but I think "usual coherence theorems" are usually understood as referring to structures which are 2-monadic over $\textsf{Cat}$, or sometimes over the 2-category of categories, functors, and natural isomorphisms. Kelly tried to pin this down further in terms of clubs, where one can in a sense reduce coherence problems to the study of the free structure generated by a single object.

Amar Hadzihasanovic (Jan 25 2021 at 23:19):

(Sorry for asking a really vague question! This is rapidly reaching the limits of what I'm confident about...)

Amar Hadzihasanovic (Jan 25 2021 at 23:24):

I don't have a strong intuition about what is 2-monadic over Cat, except that it should include all equational theories in the formal language of 2-categories, which I guess is what my intuition of “usual coherence theorems” applies to (e.g. pseudomonoids in Cat)...

Amar Hadzihasanovic (Jan 25 2021 at 23:26):

But for example I remember thinking briefly about what “free closed non-monoidal categories” look like, and that they seem something quite different from these other free algebras.

Amar Hadzihasanovic (Jan 25 2021 at 23:27):

If there even is such a thing, properly speaking...

Nathanael Arkor (Jan 25 2021 at 23:29):

There isn't a free closed category over Cat, but there is one over categories, functors, and natural isomorphisms.

Amar Hadzihasanovic (Jan 25 2021 at 23:29):

(I'll be off to sleep now, but thank you for the conversation!)

Todd Trimble (Jan 25 2021 at 23:29):

Right. These can absolutely be accommodated (Nathanael beat me to it).

John Baez (Jan 26 2021 at 02:13):

Amar Hadzihasanovic said:

So is Joyal-Street's theorem about string diagrams a coherence theorem in your opinion?

Todd has already answered, but I feel like answering too: I love that theorem, but I've never thought of it as a "coherence theorem", and I never even noticed that anybody called it a "coherence theorem".

Paolo Perrone (Jan 26 2021 at 09:08):

Speaking of "coherence": John Baez and Mike Stay seem to be using a version of string diagrams for closed monoidal categories (and then compact closed) in their Rosetta Stone, section 2.6. Can anyone tell me if we can use those diagrams for proving results? Also, are those string diagrams used elsewhere? Who was first?
I'm particularly interested in the non-compact case.

(If this is off-topic, we can move this question to a separate thread.)

Jules Hedges (Jan 26 2021 at 10:39):

John Baez said:

I never even noticed that anybody called it a "coherence theorem".

Unless I'm badly misremembering, Selinger's survey of graphical languages calls it exactly that, systematically all the way through. And almost everyone learns via that paper....

Amar Hadzihasanovic (Jan 26 2021 at 11:42):

Jules Hedges said:

Unless I'm badly misremembering, Selinger's survey of graphical languages calls it exactly that, systematically all the way through. And almost everyone learns via that paper....

You're not misremembering, it's what prompted the discussion in the first place :)

Todd Trimble (Jan 26 2021 at 12:02):

Paolo Perrone said:

Speaking of "coherence": John Baez and Mike Stay seem to be using a version of string diagrams for closed monoidal categories (and then compact closed) in their Rosetta Stone, section 2.6. Can anyone tell me if we can use those diagrams for proving results? Also, are those string diagrams used elsewhere? Who was first?
I'm particularly interested in the non-compact case.

(If this is off-topic, we can move this question to a separate thread.)

John/Mike should probably answer themselves, but the answer to the first question is: of course! More recently, Mike Shulman has been developing such string-diagrammatic aspects further; see here for a start.

Some of the basic ideas of string diagrams had precursors going far back in time, to the extranaturality graphs of Kelly and Eilenberg (late 60s), and these graphs were the basis of the really early coherence theorems for monoidal closed, monoidal biclosed, and symmetric monoidal closed categories. Kelly and Mac Lane write a paper, Coherence in Closed Categories (JPAA, 1971 or 1972 I think), which interprets morphisms in free closed categories as such graphs. Lambek's groundbreaking early work on the connection between coherence problems and proof theory interpreted these graphs in terms of a notion of "generality of proof". There was also a lot of work on this sort of thing in the Australian school in the early 1970s.

Later these graphs were reincarnated in linear logic, in the form of proof nets.

Paolo Perrone (Jan 26 2021 at 12:32):

Todd Trimble said:

John/Mike should probably answer themselves, but the answer to the first question is: of course! More recently, Mike Shulman has been developing such string-diagrammatic aspects further; see here for a start.

Oh wow, how could I miss that talk? Thank you SO much! This seems to be exactly what I'm looking for.

John Baez (Jan 26 2021 at 15:30):

Paolo Perrone said:

Speaking of "coherence": John Baez and Mike Stay seem to be using a version of string diagrams for closed monoidal categories (and then compact closed) in their Rosetta Stone, section 2.6. Can anyone tell me if we can use those diagrams for proving results? Also, are those string diagrams used elsewhere? Who was first?

I made them up for a course I taught on classical and quantum computation - see the notes for week 4 and subsequent weeks.

We didn't turn them into a systematic tool for proving things. To do that, one would need to think about the rules for nested bubbles. I don't guarantee that it's possible!

As you probably know, Mike Shulman has introduced his own string diagrams for closed monoidal categories, which have more of a theoretical footing. It would be interesting to see if they're fun to use in practice.

Mike Shulman (Jan 26 2021 at 15:42):

Amar Hadzihasanovic said:

I think the positions are:

• Mike: to solve a coherence problem is to give a presentation of the free model of a theory.
• Me: to solve a coherence problem is to characterise what morphisms are equal in a syntactic model of a theory (wrt a presentation).
• Todd: to solve a coherence problem is to give a decision procedure for equality of morphisms in a syntactic model of a theory (wrt a presentation).

I certainly wouldn't insist that a solution of a coherence problem entail an algorithmic decision procedure, although in practice they often do, and those that do are certainly more useful. But I think there's room for coherence in a mathematical sense that isn't necessarily computational. It's true that without a condition like decidability, there's room for debate in how "explicit/concrete" a "characterization" is, and I would certainly agree that coherence is a continuum rather than a binary choice.

But while I hate to burst a bubble, so to speak, I don't think I agree with your characterization of my position. It's true that to me a free model is the image of a left adjoint to a forgetful functor, but a syntactic model of a presented theory (quotiented by the relations of the theory presentation) is always, almost tautologically, such an object. Thus, to characterize equality of morphisms in a syntactic model is precisely to give an explicit description of a free object. I presume that by "characterize" you mean a characterization that is more explicit/concrete than the tautological description as a syntactic model, and I would also make that requirement: the syntactic model of a presented theory is certainly a presentation of the initial model, but I generally wouldn't regard it as solving a coherence problem.

Amar Hadzihasanovic (Jan 26 2021 at 16:28):

I agree with everything. I meant the three positions to be in increasing order of strength: everything that Todd would consider a solution to a coherence problem is also a solution for me, and everything that I would consider a solution is a solution for you too. Which is consistent with what sparked the discussion (that some of us would not include Joyal-Street in the continuum of coherence, but you would). In any case, I understand your opinion much better now and I can see that the distinction is much more subtle than I thought at the beginning.

Amar Hadzihasanovic (Jan 26 2021 at 16:37):

As in, we agree on the basic ingredients to “the solution of a coherence problem” and there are only slightly different opinions on how 'computational' the content should be. I think there are two main aspects, correct me if I'm wrong:

• does the presentation need to be finite or recursive?
• does there need to be a decision procedure for equality in the presented model?

Of course if we can say “yes” to both it is the best scenario. But I am willing to call something a solution even if it's “no” on the second, and you are willing to call something a solution even if it's “no” on both (e.g. in the Joyal-Street case where equality is presented by “all ambient isotopies of diagrams”).

Mike Shulman (Jan 26 2021 at 17:31):

Oh, is that the only difference? You only object to considering string diagrams a coherence theorem because ambient isotopy isn't finite/recursive?

Amar Hadzihasanovic (Jan 26 2021 at 19:31):

Yeah, that actually seems like a silly distinction to make. I think you are convincing me, sorry, just bear with me for a little longer. :)

Amar Hadzihasanovic (Jan 26 2021 at 19:49):

I'd like to propose some definitions that I think can work as a common ground.

• Coherence is with reference to some fixed "free model" functor $F$ (possibly for a "stricter" theory).
• A presentation of a theory determines some other functor. Let's call it $P$. Then $P$ is coherent (or has the coherence property) with respect to $F$ if we have a natural transformation $P \to F$ (or maybe just some indexed family of comparison maps?) whose components are all “acyclic fibrations” in some sense.
• A coherence theorem for $P$ is the theorem that $P$ is coherent with respect to $F$. When the components are all isomorphisms that is the same as a soundness and completeness theorem!
• The coherence problem for $F$ is the problem of finding $P$ which is coherent with respect to $F$.

Mac Lane: $F$ is “syntactic strict monoidal category”, $P$ is “syntactic monoidal category”, and the quotient maps $Px \to Fx$ are not isomorphisms but are monoidal equivalences.
Joyal-Street: same $F$, but $P$ is now “string diagrams modulo ambient isotopy”, and the comparison maps are isomorphisms (so we are in the case where coherence = soundess and completeness).
Does this make sense?

Amar Hadzihasanovic (Jan 26 2021 at 19:51):

So maybe my issue was, after all, just that the “coherence theorem” in the case of Joyal-Street is of the kind where proving a coherence theorem = proving a soundness and completeness theorem.

Amar Hadzihasanovic (Jan 26 2021 at 20:19):

So now I think that you have “the coherence problem for $F$” and “the coherence property of $P$ with respect to $F$” -- that is, the subjects of the 'problem' and the 'property' are different subjects... which I think may be the source of some of the confusion!

Mike Shulman (Jan 26 2021 at 21:52):

I suppose. I'm wary of trying to give any too-formal definition of an informal term like "coherence".

Amar Hadzihasanovic (Jan 26 2021 at 22:32):

Sure! Not trying to “fix” a formal definition, just trying to see if our informal understanding is in the ballpark of those definitions.

Amar Hadzihasanovic (Jan 26 2021 at 22:33):

Thank you for your time, it was useful for me to clarify my thoughts. I hope it wasn't a complete waste of time for you.

Mike Shulman (Jan 26 2021 at 22:49):

No worries, you made me think some too, which is always a good thing.