COHERENCE AND NON-COMMUTATIVE DIAGRAMS IN CLOSED CATEGORIES

variance. If we identify shapes with allowable functors via CJV , then the

allowable graphs (between shapes) of [11] (in [11] they are defined direct-

ly, by certain inductive rules) "are" the graphs of the allowable natural

transformations; in other words, an allowable graph £:S — T between

shapes is the graph obtained when, in the graph of an allowable natural

transformation h:pv(S) —*~ fv(T) , we replace every 1„ of the domain and

codomain by 1. As in [11],we easily see that the category (UG of shapes

and allowable graphs makes sense and is a closed category.

We now define a class JC of (formal) arrows between shapes, by de-

fining that, for any shapes A,B,C ,

a

"ABC

*ABC

bA

\ l

CAB

dAB

eAB

1 A

(AHB)HC -

AH(BHC) -

AHI -*• A

A -*- AHI

AHB -*

A -*- [B,AHB]

[A,B]HA -^ B

A —- A

AH(BHC)

(AHB)SC

are (formal) arrows between shapes (i.e. we define each such arrow as the

formal triad formed by its name, its domain and its codomain), and requir-

ing that JV consist precisely of all such formal arrows a

ABC *ABC

b,

~AB

:LR , eAr , 1A for all shapes A,B,C. The elements of 3£

will be called formal simple instances of elements of {a,a ,b,b ,c,d,e,l]

between shapes. In particular, for any shape A, 1A:A ~^"A will be called

the formal identity arrow of A. It will always be clear from the context

whether the symbol 1 denotes an identity arrow or a shape. We will often

omit the shape-subscripts on the names of elements of OT , as being clear

from the context.

We next need the formal analog of the expanded instances of a, a" ,

b, b , c, d, e and (trivially) 1.

Let S be a shape. Suppose that, in S, precisely one variable is re-

placed by the name of an element x of Jt , each one of the other vari-

oo '

ables (if such exist) is replaced by the name of the formal arrow 1- , (the