On 6/22/11 6:00 PM, Casey McCann wrote:

On Wed, Jun 22, 2011 at 2:19 PM, wren ng thornton wrote:

...

...

...

[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?

It should. But let's make sure... A coproduct of A and B is an object A+B along with morphisms inl :: A -> A+B and inr :: B -> A+B, such that for any object C and morphisms c1 :: A -> C and c2 :: B -> C, there exists a unique c1|||c2 :: A+B -> C such that c1|||c2 . inl = c1 and c1|||c2 . inr = c2. All of this is the straightforward dualizing of products. So, lets assume A ~ A+A. And lets assume we have some functions inl and inr. Now, for every pair of functions f, g :: A -> C we must come up with a unique function h :: A+A -> C such that h . inl = f and h . inr = g. By isomorphism this is the same as coming up with a unique function h' :: A -> C such that h' . iso . inl = f and h' . iso . inr = g. If inl = inr, then it follows that f = g. Consequently there can only be one morphism between any two objects, so the category is a preorder. If the category has all coproducts then it's a join-semilattice--- exactly dual to the meet-semilattice case for products. If we want a category more interesting than a preorder, then we must have that inl and inr are different. We must find two injection functions which keep their images in A+A apart, so that we can define partial functions -|||g and f|||- which don't conflict with each other (so that they can be combined into the total function f|||g). The obvious way to do that is to use tagged/disjoint unions, but we can't do that since we've assumed A ~ A+A. Basically, the type A+A isn't big enough (whereas before, the values of type A*A weren't big/informative enough). I'm playing a bit fast and loose with the notion of "big/informative enough". Perhaps someone more familiar with large ordinals can come up with a counter example. But if they do, I'm sure it wouldn't be a very intuitive place to program in. -- Live well, ~wren