On the conditions of full coherence in closed categories (Q757581)

When category theorists realized that not all diagrams commute, they invented coherence. Do at least all ``reasonable'' \((=coherent)\) diagrams in ``good'' \((=symmetric\) monoidal closed or SMC) categories commute? Unfortunately, the answer again was ``no''. The present paper offers a glimpse of hope. The author provides us with a surprisingly simple and elegant characterization of those SMC categories \({\mathcal V}\) in which all diagrams that can be built from the basic data of an SMC category do indeed commute. Such diagrams are called allowable. The first part of this characterization requires that the first dual \(A^*\) of any \({\mathcal V}\)-object A is isomorphic to the third dual \(A^{***}\). The second part may be viewed as a cancellation property for hom's in adjoint variables of allowable arrows with the same domain and codomain and the same instantiation pattern for variables, i.e., the same shape. Both conditions follow if any \({\mathcal V}\)-object A is isomorphic to its second dual \(A^{**}\), as is the case in the category of finite dimensional vector spaces, but the converse does not hold. The nontrivial proof of the characterization theorem is very carefully mapped out. The proof-theoretic techniques employed are at least as interesting as the results themselves, opening the door for further fruitful interactions between logic and category theory.