COHERENCE AND NON-COMMUTATIVE DIAGRAMS IN CLOSED CATEGORIES

S -^ T are two arrows of ^ , then h = hf if and only if h = ^(P) = h1 for

some normal proof P of G; this result is then combined with the fact ([17])

that the set of all normal proofs P:S -^ T in G is finite and computable.

In our treatment of the problem we follow the methods of [11], espe-

cially of the formulation of their "cut elimination" theorem ([11, Theorem

6.5, via Propositions 6.2 and 6.4]) and its use in proofs by induction.

Kelly-MacLane, in their introduction ([11]), attribute their inspiration

on this idea to Lambek's work ([12],[13]) who, in turn, was inspired by the

work of Gentzen ([7]). In the remainder of this introduction, we give some

details of this method, as it appears in [11],in order to introduce the

ideas and the notation that we will use.

We start with the known facts ([6],[8],[14]) about monoidal catego-

ries (or, symmetric monoidal categories); these categories are defined by

the data which remain when, in the definition of closed categories given

in the beginning of this introduction, we omit [,] in (ii),omit (v) and

omit C5 and C6 in (vi).We know that monoidal categories are coherent, i.e.

in them, any two composites of instances of elements of {a,a~ ,b,b" ,c,l]

are equal if and only if their graphs are the same. A closed category is,

in particular, a monoidal category. Those allowable (canonical) arrows in

a closed category, which are composites of instances of elements of {a,a ,

b,b ,c,l} only, are called central arrows. The central arrows of ^ will

be simply called central natural transformations. So, in the language of

(III), the above fact is stated as follows:

if h,h!:S —•T are central natural transformations (between shapes),

then h = h' if and only if |~ h = ThT .

We next observe that the axioms C5 and C6 on d and e imply that, for

any objects A,B,C of a closed category C , there is an isomorphism

TT: Homc(ABB,C) -*• Homc (A, [B,C])

which is natural in A,B,C and where

?r(f) is the composite A — ^— ^ [B,ASB] — [ 1 ? f ^ [B,C]

and

ir~ (g) is the composite A$B

gB1

[B,C]SB —^-^ C .

xiii