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.

StackExchange Computer Science Q#70530, answer score: 4