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