Todd Wilson <twilson@csufresno.edu> wrote:
- Although we constantly speak of "the" product, we really only have "a" product (at least if we take the category-theoretic perspective seriously). What is really involved, formally, in making the move from "a" to "the"? A formal language translation scheme? Coherence theorems? How much technical work is really involved here?
Actually, nothing is involved if we introduce a product operator. That is, we take operators _x_, p0_,_ p1_,_ and say: For any objects (or types) A and B the object AxB has arrows p0A,B:AxB --> A and p1A,B:AxB -->B with the properties of a categorical product. Notice that the categorical property is exactly what you want in a product type: From a record of type AxB you can recover the A entry, and the B entry, via the projections. And whenever you have a pair of values, one in A and one in B, there is a correspondng single value in AxB. Notice, the "values" may be parametrized, so we are actually dealing with operations f:T-->A and g:T-->B and the resulting (f,g):T-->AxB. Then AxB will generally not be the only product of A and B in the category, but it will be one, and that is what we need. Coherence theorems indeed are important. But they are provable from the above. So there is no need to give them as part of specifying the product--the same as a computer need not have the Chinese remainder theorem programmed into it, to implement arithmetic.
- Related to this, what about the fact that if
(pi0: A x B -> A, pi1: A x B -> B)
is a product, then so is (pi1, pi0), indistinguishable categorically from the other product?
Sadly, that is not a fact. The pair (pi0,pi1) gives a product of A and B, while (pi1,pi0) gives a product of B and A. This is revealed categorically by the fact that the codomain of pi0 is A, while the codomain of pi1 is B. In programming terms, a data record of <your age in years, your height in inches> is different from a record of <your height in inches, your age in years>. It is quite important practically, as well as theoretically, to distinguish the product of A and B from that of B and A. Even in a product BxB we need to keep the projections in order. For example, that is how we distinguish between pairs <x,y> of reals with x less than y, and pairs <x,y> of reals with y less than x. An important distinction. This is why a correct specification of the categorical product specifies the projection arrows as p0_,_ p1_,_, or in words: "projection to the first of the following two objects" and "projection to the second of the following two objects"
- Is there anything to be made of the fact that the set-theoretic cartesian product is a local construction, involving only the sets A and B and certain small sets made up of their elements, whereas a/the category-theoretic product depends on the whole category (because of the quantification in the universal property)?
This is one reason why a computer implementation of the categorical product, in any reasonably rich environment, will be incomplete. But it pales beside other reasons why computer implementations of any reasonably strong construction are incomplete. The ZF set-theoretic product will also be incomplete in any computer implementation Compare the way Goedel's theorem shows that computer implementations of arithmetic will all be incomplete. It pales beside the fact that normal implementations don't try to implement induction at all.
And, finally, shouldn't "better" really be "better for what"? In other words, aren't the two communities really just arguing past one another, like people arguing over types of automobile? What really is the issue here?
There are many different issues, and correspondingly different arguments. Which one did you mean to address?