COHERENCE AND NON-COMMUTATIVE DIAGRAMS IN CLOSED CATEGORIES

(i) naturality of the arrows

(ii) functoriality of S and [,]

(iii) the axioms of the closed structure on a,a ,b,b ,c,d and e.

These additional conditions are given in the form of equalities between ar-

rows of U , in the spirit of making the formal instances behave like real

instances of elements of [a,a ,b,b ,c,d,e} in U .

Let y be the (smallest) equivalence relation on X = Arr2^ generated

by the equalities establishing exactly (i),(ii) and (iii) above and compat-

ible with ®, [,] and composition in Ot . Then we define & = V- ly ( Obj^=

0bj2( , Arr#~ = Ot/y ). The arrows of $* will be called abstract allowable

natural transformations between shapes.

^ is a free closed category with one generator (the shape 1).If

f:S —-T is in ^ , i.e. f:S--T is a formal instance between shapes of

an element y of {z,*'1,b yb'19c,d9e,1}9 then [f]^:S --T (the ^-class of f)

is a real instance of y in the closed category #~. In practice, an arrow

of #" (which is a ^-equivalence class of arrows of U ) is given via one

of its representatives, i.e. as [h . . .h^h^y with hn. . .h^h-^eTt (and [z]y

denoting the J^-class of z). Then

[hn...h2h1]y = [hn]y. ..[h2]y[h1]yr ,

so we may also say that an arrow of #" is given as a composite of (ordina-

ry or expanded) real instances in #~ of elements of {a,a ,b,b ,c,d,e,l}.

From now on, the term allowable natural transformation, when used

with shapes as domain and codomain and without reference to any closed cat-

egory, will always mean an arrow of & in the present paper.

The coherence problem for closed categories is now stated as the co-

herence problem for the category $~ , in which all the arrows are canonical,

as follows:

(III) When are two allowable natural transformations (between shapes)

with the same domain and the same codomain equal ?

If y is any closed category, let CttN(V) be the closed category of

allowable functors and allowable natural transformations (with respect to

V ). There is a unique strict closed functor F„: fr -~ (UN(V) which sends

the shape 1 to the functor ly and every instance in §? of an element x of

xi