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: theory: category theory

Topic: General formulation of coherence conditions

Patrick Nicodemus (Apr 24 2024 at 21:13):

I've been looking for general formulations of the concept of "coherence conditions" which allow us to say, for a given proposed categorical structure, what the "right" coherence conditions should be.

I do feel that I can usually write down the appropriate coherence conditions without trouble, based on my intuition. A good sanity check here is that one can derive an appropriate "coherence theorem"; the question is essentially, do we have a fairly general description of what the coherence theorem should state in the case of an arbitrary given structure.

An example I've been thinking about is a biadjunction between bicategories. The important additional coherence condition here beyond the 1-categorical case is the so called "Swallowtail identity". I am not confident I can write down the correct coherence theorem here describing all diagrams that commute in the biadjunction.

One cannot just say "all diagrams commute", of course. A basic example: let C be a category, c be an object and f : c -> c. Then the coherence theorem for a category does not imply that $f\circ f=f$. So, not all diagrams commute.

Perhaps the problem here is linearity, the fact that $f$ occurs twice on the right. Indeed if we restrict to linear terms in a 1-category, any two linear well-typed terms $a \to b$ seem to be equal, i.e. $(f\circ g)\circ (h\circ k) = f\circ (g\circ h) \circ k$. (assuming that the identity morphism and other constants are nonlinear so we can use them as many times as we want.)

However there are other problems beside linearity. If $t:a\to a$ is a monad in a 2-category $B$ then there are two maps $\mu\cdot \operatorname{id}_t, \operatorname{id}_t\cdot \mu : t^3\to t^2$ and these do not commute. One only has that all maps $t^k\to t$ commute where $k$$ is arbitrary. "Linearity" appears here only indirectly in the requirement that $t$ must occur exactly once on the right hand side of the arrow, but not on the left.

One trick I thought of to solve this is to treat the 2-category as a virtual double category instead of a 2-category. Then we cannot even state the condition $\mu\cdot \operatorname{id}_t= \operatorname{id}_t\cdot \mu : t^3\to t^2$ as it is not well typed (all 2-cells in a virtual double category must have a single cell as their codomain.)

But this trick makes us unable to state well known coherence conditions such as the pentagon identity or triangle identity for monoidal categories and bicategories, and it seems like an unsatisfying answer to the original question to rule out Mac Lane's coherence theorem as an example of coherence.

So, my conclusion here is that, working in some appropriate linear dependent type theory, "any two terms of the same type should be equal" gives the right coherence conditions in some cases, but is insufficient in others.

Ryan Wisnesky (Apr 24 2024 at 23:34):

in type theory we call coherence conditions "congruence rules" https://ncatlab.org/nlab/show/congruence+rule and they often arise when you want all your term formers to respect/be closed under all the other term formers. Like, you have enough congruence rules when you can actually build a congruence relation out of terms. There's also the notion of "logical harmony" https://en.wikipedia.org/wiki/Logical_harmony

Patrick Nicodemus (Apr 24 2024 at 23:51):

I do not understand what you mean. It's not clear to me how coherence conditions in category theory are equivalent to congruence rules in the link you posted. Do you have a simple example of this correspondence?

Ryan Wisnesky (Apr 25 2024 at 00:31):

I'm trying to answer the question, 'where do coherences such as MacLane's pentagon identity come from'. IMO, they come from deep analysis of what is being axiomatized. For example, MacLane's pentagon identity isn't obviously related to the monoid axioms, but it is obviously related to the 'completion' of the monoid axioms into a convergent re-write system (it comes from analyzing 'critical pairs'). Similarly, many coherences come from closing specific equivalence relations on terms under congruence. Here's a paper describing the former in detail https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=3a0a21aa1c60381537370967bbc900166bd67ebf . "From the viewpoint of term rewriting, what coherence axioms define is a congruence between proofs with respect to which any equational identity possesses a unique equivalence class of equational proofs (i.e. sequence of rewrites from left-hand to right-hand side)" and "research on coherence inevitably becomes research on word problems"

Brendan Murphy (Apr 25 2024 at 01:08):

What a nice paper!

Patrick Nicodemus (Apr 25 2024 at 03:59):

It's incorrect that all linear terms in a category are equal. If $f,g : c\to c$ then $gf\neq fg$ in general. It would seem that the strongest thing we can say is that all definable functions
$\prod_{x_0,x_1,\dots x_n} Hom(x_0,x_1)\times\dots Hom(x_{n-1},x_n)\to Hom(x_0,x_n)$ are equal.
Linearity might be a red herring here as it just so happens that the only functions so definable are linear in each coordinate.

Amar Hadzihasanovic (Apr 25 2024 at 06:27):

I would say that, in all generality, a statement of "coherence" is the statement that a certain object is contractible; usually a "free" (or cofibrant, when that makes sense) object.

Thus it relies on a few choices:

• what it means to be contractible — categorically this usually means that we are at least in a category with weak equivalences with a "point" object, typically the terminal object so that contractibility is the statement that the unique map to it is a weak equivalence;

• and, of course, what is the object that we want to be contractible.

Note that in many cases rather than "this object is contractible" it will be more natural to phrase coherence as "this morphism is a weak equivalence" but the latter can be turned into the former by passing to slice categories, similarly to how every statement that "a cone is a limit cone" can be turned into the statement that "an object is terminal"

Amar Hadzihasanovic (Apr 25 2024 at 06:31):

The typical situation where we want coherence is when we are replacing "equality" by "coherent equivalence", in which case we are saying that the map that "quotients" the space of witnesses of equivalence down to a single point, which witnesses "identity", is contractible.

Amar Hadzihasanovic (Apr 25 2024 at 06:34):

That this is related to convergence in rewrite systems is a consequence of the duality between higher-dim rewriting and homotopy, as studied e.g. in the theory of polygraphs. However "convergent" coherence is in general stronger than just coherence, as it asks for contractibility to be witnessed by a "directed" homotopy...

Amar Hadzihasanovic (Apr 25 2024 at 06:39):

For example coherence for monoidal categories using only the pentagon & triangle cannot be proved with a convergent higher-dim rewrite system, I think. You need three more cells for that, as there are, iirc, 5 critical pairs in the rewrite system determined by unitors and associators...

Amar Hadzihasanovic (Apr 25 2024 at 06:41):

And indeed this was Mac Lane's original formulation, before Kelly was able to show that 3 of those could be constructed from the rest — but this proof uses essentially the fact that unitors and associators are isomorphisms and does not extend to, e.g. lax monoidal categories.

Amar Hadzihasanovic (Apr 25 2024 at 07:01):

Actually I've changed my mind about one point that I've made: in practice, the fact that coherence statements of the form "a certain morphism is a weak equivalence" can be turned into statements of the form "a certain object is contractible" is not due to passing to global contractibility in a slice, but rather because being a weak equivalence can often be checked locally by proving that all fibres are contractible.

Amar Hadzihasanovic (Apr 25 2024 at 07:03):

I think this is truer to the case e.g. of monoidal categories, where the statement that the quotient functor from the free monoidal category to the free strict monoidal category on a set of objects is proved by showing that the fibre over each object is a contractible groupoid...

Patrick Nicodemus (Apr 25 2024 at 13:51):

A nonempty contractible groupoid furthermore. So an acyclic fibration. Small detail but I've been thinking lately about how this extra condition helps.

Patrick Nicodemus (Apr 26 2024 at 19:18):

For the record, I believe that the statement

In type theory we call coherence conditions "congruence rules"

is simply incorrect, if "congruence rules" are understood in the sense of the linked nlab page. In my opinion the linked nlab page is a red herring and is irrelevant to the conversation, perhaps a different notion of "congruence rule" was meant which does not concern definitional equality in dependent type theory.

The notion of "congruence" that appears in the linked paper is used in the broad sense of a "congruence relation" which basically just means "an equivalence relation compatible with relevant algebraic structure".