On Wed, Jun 22, 2011 at 2:19 PM, wren ng thornton
[1] modulo the A:+:A ~ A issue.
Oops, I should've said A:*:A there.
That issue is exactly my concern, though, and it seems a bit too thorny to handwave aside.
Indeed. If we have A:*:A ~ A, then A:*:A is not a categorical product. (...)
Thank you, that clarified my intuitive sense of why it didn't seem to work. The same argument, with arrows flipped appropriately, would apply to a hypothetical coproduct where A :+: A ~ A, wouldn't it?
Disjoint pairs are sufficient; they needn't be ordered. All we need is that they are "tagged" in the same way that disjoint unions are, so that we can distinguish the components of A*A.
Oh. Yes, of course, I probably knew that. I think confused myself by habitually calling the components "fst" and "snd". Sigh. - C.