[PRL] IOP and disjoint unions

[Dave Herman]

>>I don't get this.  I don't know anything about category theory, but it
>>seems like "an apple or an apple" is always the same as "an apple".
> 
> It is, for a suitable definition of "or" that has little if
> anything to do with the disjoint union signified by the plus
> sign above.  (See subject line.)

Somewhat more concretely, in set theory disjoint union is usually 
encoded using a "tag" to distinguish between the two cases:

     A + A = ({ 0 } x A) U ({ 1 } x A)

     injectLeft : A -> A + A
     injectLeft(a) = (0, a)

     injectRight : A -> A + A
     injectRight(a) = (1, a)

The set { 0 } x A is not the same as A, nor is the set { 1 } x A the 
same as either of the other two.

Naturally, the categorical definitions are more abstract, much like the 
mustard watch is more abstract than the classical watch:

     http://iml.univ-mrs.fr/~girard/mustard/article.html

Dave