COHERENCE AND NON-COMMUTATIVE DIAGRAMS IN CLOSED CATEGORIES

It is clear that, in (ii) , (iii) and (iv) above, each one of f and g has

rank smaller than the rank of h, and on this fact the inductive argument

can be based.

In [11],we work with C being one of the categories G (the category

of shapes and graphs) and N = N(y) (the category of shapes and ordinary

natural transformations with respect to a closed category y). With the aim

of proving the main theorems by induction on rank, the main idea is to show

that the class of allowable arrows of C has the above cut elimination prop-

erty. For this purpose we consider the class of constructible arrows of C;

this is the class generated by the central arrows of C and closed under the

above four processes of construction; we easily see that it has the cut e-

limination property. Then we show that this class coincides with the class

of allowable arrows. The main point in proving this, is to prove (by induc-

tion on ranks, using the cut elimination property of constructibles) that

the class of constructible arrows is closed under composition. This fact

is essentially the cut elimination theorem (of [11]) , although we often

call "cut elimination theorem" the proposition which states that the class

of allowable arrows has the above cut elimination property.

Modifications of this cut elimination property and corresponding new

cut elimination theorems (with respect to different processes of construc-

tion) will be our basic tools in the present paper.

We often say that an arrow h of C is of type (or, of the form) $ , ir

or , if h satisfies (ii) , (iii) or (iv) of the above cut elimination

property, respectively, with (B being the class of allowable arrows of C.

The techniques of [11] involve also the idea of prime factorization

of shapes, which we repeat here, since it will be used in the sense of [11]

in Part One and in §1 of Part Two of this paper. The prime shapes are the

shape 1 and all shapes of the form [R,T]. The integral shapes are those

shapes which do not involve [,] . The inductive definition of shapes im-

plies that any shape S is gotten by the substitution of prime shapes for

the variables in some integral shape; these prime shapes are the prime fac-

tors of S. In other words, a prime factor of S is a prime subshape K of S

which is not a subshape of any prime subshape of S different from K itself.

xv