Origin

HoTT Zulip: terminology discussion.

References

Wikipedia

[A] coherence condition is a collection of conditions requiring that various compositions of elementary morphisms are equal.

Wikipedia has a hilariously bad example that makes no sense, but then they give a diagram that… actually does? Recapitulating it:

\[ \xymatrix{ ((A \otimes B) \otimes C) \otimes D \ar[r] \ar[d] & (A \otimes (B \otimes C)) \otimes D \ar[r] & A \otimes ((B \otimes C) \otimes D) \ar[d] \\ (A \otimes B) \otimes (C \otimes D) \ar[rr] && A \otimes (B \otimes (C \otimes D)) } \]

Where the point is that if you have this diagram, then you /have coherence/—you don’t need to prove it \(\forall c \in C\).

nLab

While associativity and uniticity of composition of k-morphisms holds only up to choices of higher morphisms, coherence is the demand that the collection of these choices forms a contractible -groupoid.

jfc

A little more than half-way down the page and we’re talking about Trimble \(\omega\) categories and yeah, I’m out.

Intuition

Induction

What is coherence’s relationship to induction? Going back to diagram given in the Wikipedia section of this document and I’m thinking… could there be a way to express that diagram inductively? A type with four parameters where each constructor is a different associative configuration and then a proof that \(\forall (m\ n : \text{MCoherence}) \rightarrow m \equiv n\)?