R.VOREADOU

{a,a" ,b,b ,c,d,e,l} to the corresponding instance of x in tf£N(Y). For a

shape S, FV(S) is precisely the functor |S| of [11,pp.103-104]. The compo-

nents in V of an (abstract) allowable natural transformation h between

shapes are the (ordinary) components in V of the (ordinary) allowable nat-

ural transformation Fv(h) .

QtG is a closed category and there is a strict closed functor $:

flIN(fl£G) —- fllG which sends the functor lnfC to the shape 1, the constant

functor I: Q1G —• I to the shape I and each arrow k of 2£N(#XG) to the graph

which is the component in MG of k gotten when we take each argument in the

domain and codomain of k equal to the shape 1. The composite P^non will be

denoted by [ ; this is a strict closed functor r: $* -*- (JUL G which is the

identity on objects and, for any (abstract) allowable natural transforma-

tion h:S —»- T between shapes, its graph |~h is the component, with domain S

and codomain T, of h in OULG .

It is then clear that two allowable natural transformations h,hf:

S —• T (between shapes) can be equal only if Th = |~h' and, in case [" h =

rh1,

then h =

h1

if and only if, in every closed category V , h and

hf

have the same components (for each choice of arguments for the functors

Fy(S) and Fy(T) according to the graph Th = Th! ).

In the present paper, we answer the question (III) by giving a finite

necessary and sufficient condition for two allowable natural transforma-

tions with the same domain, the same codomain and the same graph to be e-

qual. This is based on two items: first, a class Of of pairs

(h,hf)

of al-

lowable natural transformations with d h = 3 hT , 3-h = 9.,hT and f" h = Th1

o o ' 1 1

and, second, a closed category ft , which are so defined that

1) (h,h')€3^ implies h f

hf

because, for (h,h')€^, certain components

in J^ of h and hf are different

2) (h,h T )^ implies h = hf

3) h = hf can be tested by testing equality of a finite number of compo-

nents of h and

h!

in ^ in a finite number of steps.

Question (III) is also considered in [16], where an isomorphism G :

G -- p is established between fr (the F(l) of [16]) and a deductive sys-

tem G, so that arrows of & correspond to normal proofs in G; if h,hf: