COHERENCE AND NON-COMMUTATIVE DIAGRAMS IN CLOSED CATEGORIES
(i) naturality of the arrows
(ii) functoriality of S and [,]
(iii) the axioms of the closed structure on a,a ,b,b ,c,d and e.
These additional conditions are given in the form of equalities between ar-
rows of U , in the spirit of making the formal instances behave like real
instances of elements of [a,a ,b,b ,c,d,e} in U .
Let y be the (smallest) equivalence relation on X = Arr2^ generated
by the equalities establishing exactly (i),(ii) and (iii) above and compat-
ible with ®, [,] and composition in Ot . Then we define & = V- ly ( Obj^=
0bj2( , Arr#~ = Ot/y ). The arrows of $* will be called abstract allowable
natural transformations between shapes.
^ is a free closed category with one generator (the shape 1).If
f:S —-T is in ^ , i.e. f:S--T is a formal instance between shapes of
an element y of {z,*'1,b yb'19c,d9e,1}9 then [f]^:S --T (the ^-class of f)
is a real instance of y in the closed category #~. In practice, an arrow
of #" (which is a ^-equivalence class of arrows of U ) is given via one
of its representatives, i.e. as [h . . .h^h^y with hn. . .h^h-^eTt (and [z]y
denoting the J^-class of z). Then
[hn...h2h1]y = [hn]y. ..[h2]y[h1]yr ,
so we may also say that an arrow of #" is given as a composite of (ordina-
ry or expanded) real instances in #~ of elements of {a,a ,b,b ,c,d,e,l}.
From now on, the term allowable natural transformation, when used
with shapes as domain and codomain and without reference to any closed cat-
egory, will always mean an arrow of & in the present paper.
The coherence problem for closed categories is now stated as the co-
herence problem for the category $~ , in which all the arrows are canonical,
as follows:
(III) When are two allowable natural transformations (between shapes)
with the same domain and the same codomain equal ?
If y is any closed category, let CttN(V) be the closed category of
allowable functors and allowable natural transformations (with respect to
V ). There is a unique strict closed functor F„: fr -~ (UN(V) which sends
the shape 1 to the functor ly and every instance in §? of an element x of
xi
Previous Page Next Page