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
Previous Page Next Page