One might say that the ordering of binary products, with a first
projection
and a second projection, is spurious but inevitable.
The two components of a binary product must be distinguished, as Colin McLarty explained, but they must be allowed to be isomorphic. The usual way we handle a situation like this in mathematics is to index them, in this case by a two-element set. ...
Two points. First, even in computer programming, one can lose the need for an ordering by using what are often called "record types", so that <your age in years=99, your height in inches=70> denotes the same record as <your height in inches=70, your age in years=99> I don't think there's anything mysterious about this. A pair of sets can be described as a function f: X -> 2, and we can quite happily replace 2 by any isomorphic set (but we don't have to choose the isomorphism) such as M = {"your height in inches", "your age in years"} The product of f: X -> M is then a universal solution to the problem of finding g: YxM -> X over M and this is equivalent to the usual characterization once you have chosen the isomorphism between M and 2. A second, and deeper, point is that constructively there are unorderable 2-element sets, so there is a kind of binary product in which the ordering first vs. second projection is impossible. It uses the same "record type" construction. An example in sheaves over the circle O is the twisted double cover M (edge of a Mobius band). It is finite decidable set with cardinality 2. It is isomorphic to 2 (i.e. 2xO) locally but not globally. It has no global elements and no global total ordering. If you have a sheaf X with a map f: X -> M, then locally it falls into two parts whose product you can take. It can be expressed as Pi f = {(i,x,j,y) in MxXxX | f(x) = i and f(y) = j and j = s(i)} / ~ where s: M -> M swaps the two elements and ~ is the equivalence relation generated by (i,x,j,y) ~ (j,y,i,x). Globally, Pi f is the equalizer of two maps from X^M to M^M, namely f^M and the constant identity map: so set theoretically it is the set of sections, {g: M -> X | g;f = Id_M} The universal property is that for any YxM -> X over M you get a unique corresponding Y -> Pi f. The second description with X^M probably looks more natural to a topos theorist, but the first one has the advantage of being geometric. Steve.