Goldblatt, /Topoi/: definition of exponentiation


Binary products in a category have been defined by Goldblatt in the
standard way: a product of objects a and b is an object c along with
arrows p: c -> a, q: c -> b, satisfying a universal property. The
quasi-functional notation a x b is used from the start, and this is
distracting, but can be ignored, in the context of simple exercises
such a proving (a x b) x c =~= a x (b x c). However, in the context
of the definition of exponentiation in section 3.16, the notation
seems to play an essential role.

It is one thing to say that a category has binary products in the
sense that for any ordered pair of objects a, b, there exists an
object c which is a product of a and b. It is another thing to say
that there exists a binary operation on the collection (set? class?)
of objects of the category which constructs a particular such object
a x b from each ordered pair a, b.

The definition of exponentiation only seems to make sense on the
understanding that there exists such a definite binary operation
that constructs binary products of pairs of objects. One can proceed
with reading the text and understanding it in a normal logical way
if one assumes that when a category is said to have binary products,
what is meant is that, along with the unary operations dom and cod,
and the binary operation o of composition of arrows, and the unary
operation which associates an identity arrow to every object ...

....I'm trying not to make any specifically set-theoretic assumptions
here, just whatever assumptions one would have to make in order to
justify reasoning logically about categories, either formally or
informally ...

.... substitute some other more acceptable terms for "unary operation",
"binary operation", and "ordered pair", if they seem too uncomfortably
reminiscent of constructions within some formal set theory ...

.... along with dom, cod, o and 1_ there is provided a binary operation
x on the collection of objects of the category, and arrows a x b -> a
and a x b -> b, for every a, b, satisfying the universal property for
binary products.

It now makes sense to postulate that there also exists a binary
operation on objects that constructs from any pair of objects a, b
the object b^a, along with the evaluation arrow ev: (b^a) x a -> b,
satisfying the stated universal property.

So I can carry on reading the book and following the proofs, with
this understanding.

But it worries me that some kind of postulate seems to have been
sneaked in implicitly, instead of being stated explicitly. It looks
a bit like a silent use of the axiom of choice. But I have a vague
sense that what is really in the author's mind is a constructivist
subtext, which is not part of the text proper. Can anyone enlighten
me as to what is really going on here? Does one have to understand
mathematical "existence" in a certain way, in order to be comfortable
with the way in which the "existence" of binary products is being
treated here?

--
Angus Rodgers
"Out came a creature with a face like Venus: round,
lifeless, and pitted with craters."
.

Relevant Pages