Linear logic, bimodules, and full coherence for autonomous categories
Todd H. Trimble, Myles Tierney · 1994
A complete solution is given to the coherence problem for symmetric monoidal closed categories, herein called autonomous categories. Symmetric monoidal categories, introduced by Mac Lane, are categories with abstract tensor products which are associative, commutative, and equipped with a unit up to natural isomorphism; these natural isomorphisms are required to satisfy compatibility conditions, usually called coherence conditions. Symmetric monoidal closed categories, introduced by Eilenberg and Kelly, have in addition an internal hom satisfying familiar adjointness relations with respect to the tensor. A coherence problem for a given class of categories with structure calls for an algorithm which decides equality of morphisms in the categories which are free with respect to the structure, and asks: which diagrams built from the structure commute? Kelly and Mac Lane proved a partial coherence result for autonomous categories which did not address problems with the unit. The problem of the unit is addressed here by re-interpreting Girard's linear logic, and particularly his cyclic trips, in terms of bimodule actions of the unit upon other objects in the free category. We similarly interpret the more recent graphs of Danos and Regnier and extend them to handle unit isomorphisms. We form a category from the extended graphs, and construct a functor from this category onto the free category. Defining graphs to be equivalent if they map to the same morphism, the coherence problem is solved in two steps. First, we characterize equivalence geometrically in terms of rewirings, which is the principal notion of this work. Second, the principal theorems show that the system of rewirings on a graph may be arranged into a rewrite system which satisfies confluence and strong normalization properties. Some illustrative examples are given.