Distributive property with sum types and product types In Philip Wadler's presentation, "Category Theory for the Working Hacker", something confused me. At about 30:52, he says:


  We need this additional construct which is called distributivity. Here it is, right? It just says "given a choice of an A or a C and a choice of a B or a C, we can get a choice of an A or a B and a C."


This is shown on the slide as:


  $$ (A + C)\times(B + C) \cong (A + B) \times C $$


Is this correct? I have the following doubts about it:


I think that, in Boolean algebra, the distributive property would give $ (A + C)\times(B + C) = (A \times B) + C $.
Given a choice of an A or a C and a choice of a B or a C, we might choose C both times, giving us only a C and a C. For example, in Haskell:


    data AorC = ACA A | ACC C       -- sum type
    data BorC = BCB B | BCC C       -- sum type
    data Prod = Prod AorC BorC      -- product type
    cAndC = Prod (ACC c1) (BCC c2)  -- choose type C both times
Polynomial types (those obtained through $+,\times,0,1$ and type variables) form a commutative semiring. 

Basically, all the elementary arithmetic laws for $+$ and $\times$ hold as expected, up to (natural) isomorphism. These include commutativity, associativity, and distributivity of $\times$ over $+$.

More concretely, the distributive law is
$$ (A\times C)+(B\times C) \simeq (A+B)\times C$$
and I think this was the law that Philip Wadler meant to show.