COHERENCE AND NON-COMMUTATIVE DIAGRAMS IN CLOSED CATEGORIES
S -^ T are two arrows of ^ , then h = hf if and only if h = ^(P) = h1 for
some normal proof P of G; this result is then combined with the fact ([17])
that the set of all normal proofs P:S -^ T in G is finite and computable.
In our treatment of the problem we follow the methods of [11], espe-
cially of the formulation of their "cut elimination" theorem ([11, Theorem
6.5, via Propositions 6.2 and 6.4]) and its use in proofs by induction.
Kelly-MacLane, in their introduction ([11]), attribute their inspiration
on this idea to Lambek's work ([12],[13]) who, in turn, was inspired by the
work of Gentzen ([7]). In the remainder of this introduction, we give some
details of this method, as it appears in [11],in order to introduce the
ideas and the notation that we will use.
We start with the known facts ([6],[8],[14]) about monoidal catego-
ries (or, symmetric monoidal categories); these categories are defined by
the data which remain when, in the definition of closed categories given
in the beginning of this introduction, we omit [,] in (ii),omit (v) and
omit C5 and C6 in (vi).We know that monoidal categories are coherent, i.e.
in them, any two composites of instances of elements of {a,a~ ,b,b" ,c,l]
are equal if and only if their graphs are the same. A closed category is,
in particular, a monoidal category. Those allowable (canonical) arrows in
a closed category, which are composites of instances of elements of {a,a ,
b,b ,c,l} only, are called central arrows. The central arrows of ^ will
be simply called central natural transformations. So, in the language of
(III), the above fact is stated as follows:
if h,h!:S —•T are central natural transformations (between shapes),
then h = h' if and only if |~ h = ThT .
We next observe that the axioms C5 and C6 on d and e imply that, for
any objects A,B,C of a closed category C , there is an isomorphism
TT: Homc(ABB,C) -*• Homc (A, [B,C])
which is natural in A,B,C and where
?r(f) is the composite A ^— ^ [B,ASB] [ 1 ? f ^ [B,C]
and
ir~ (g) is the composite A$B
gB1
[B,C]SB —^-^ C .
xiii
Previous Page Next Page