Bicartesian closed category is distributive I want to prove that a bicartesian closed category is distributive i.e. that $(A+B)\times C \cong (A \times C) + (B \times C)$ . I first found (using properties of exponentials) that $\hom((A\times C)+(B\times C),X) \cong \hom((A+B)\times C,X)$ for each object $X$. Can I deduce more from that ?
I am not familiar with the Yoneda lemma so I would appreciate some fundamental approaches / help.
 A: Let $\alpha_X : \text{hom}((A\times C) + (B\times C), X) \simeq \text{hom}((A + B) \times C, X)$ be the isomorphism you mention. Let $\beta_X$ be the inverse of $\alpha_X$. First, try so show that $\alpha$ satisfies the following property: Given any $f : X \to Y$ and $\phi \in \text{hom}((A\times C) + (B\times C), X)$ the equation 
\begin{align}
\alpha_Y(f \circ \phi) = f \circ \alpha_X(\phi)
\end{align} (this means that $\alpha$ is a natural transformation between the two hom functors). This should be very easy to show if you've defined $\alpha$ in the obvious way.
Now to show that sums distribute over products directly you have to come up with two morphism and show that they are inverses. Since you have the bijections between the hom-sets it is easy to come up with two such morphisms. Let $U = (A + B) \times C$ and $V = (A \times C) + (B \times C)$. Take $\text{id} \in \text{hom}(V, V)$. Then $\alpha_V(\text{id}) : U \to V$ and $\beta_U(\text{id}) : V \to U$.
We need to show that they are mutually inverse. Pick $f = \beta_U(\text{id})$ and $\phi = \text{id}$. Then the equation above reduces to $\alpha_U(\beta_U(\text{id})) = \beta_U(\text{id}) \circ \alpha_V(\text{id})$ and since $\alpha_U$ and $\beta_U$ are inverses of each other we get $ \text{id} = \beta_U(\text{id}) \circ \alpha_V(\text{id})$ which shows one direction.
Applying $\beta_Y$ to the equation above we get $f \circ \phi = \beta_Y(f \circ \alpha_X(\phi))$ and since $\beta_X$ is an isomorphism there exists a $\psi$, such that $\phi = \beta_X(\psi)$ so the equation becomes $f \circ \beta_X(\psi) = \beta_Y(f \circ \psi)$. Now instantiate this with $f = \alpha_V(\text{id})$ and $\psi = \text{id}$ to get $\alpha_V(\text{id}) \circ \beta_U(\text{id}) = \text{id}$, showing that $\alpha_V(\text{id})$ and $\beta_U(\text{id})$ are mutually inverse.
Note that the above shows, more generally, that the Yoneda functor reflects isomorphisms.
A: From a technical standpoint, Zhen is correct in emphasizing adjoints; this is the simplest and most fundamental reason for the distribution of products over coproducts in the presence of exponential objects. However, from a pedagogical standpoint, sometimes it's better to give further details. A lot of category theory proofs are very abstract, which can be detrimental to understanding.
With that in mind, here's a very explicit proof that works in the category of sets directly, and which also works in any bicartesian closed category as long as you know how to replace variables with variable-free notation.
First, let's agree on some names for the canonical isomorphisms of the hom-tensor adjunction. In particular, let's call them curry and uncurry.
$$\mathrm{curry}:\mathrm{Hom}(A \times B, C) \longrightarrow \mathrm{Hom}(A, [B,C])$$
$$\mathrm{uncurry}:\mathrm{Hom}(A, [B,C]) \longrightarrow \mathrm{Hom}(A \times B, C)$$
I'll also use $\eta_i$ for the universal maps into coproduct objects. Like so:
$$\eta_1 : X \rightarrow X + Y \qquad \qquad \eta_2 : Y \rightarrow X + Y$$
With that in mind, here's an explicit proof.

Proposition/Definition 0. In any category with binary products and coproducts, there's a unique map
  $$\mathrm{factorize} : X\times Z + Y\times Z \rightarrow (X+Y)\times Z$$
  satisfying 
  $$\mathrm{factorize}(\eta_1(x,z)) = (\eta_1(x),z)$$
$$\mathrm{factorize}(\eta_2(y,z)) = (\eta_2(y),z)$$

Proof. Immediate from the universal property of coproducts.

Proposition/Definition 1. In any category with binary products, coproducts and exponential objects, there's a unique map
  $$\mathrm{expand} : (X+Y)\times Z \rightarrow X\times Z + Y\times Z$$
  with the following properties
  $$\mathrm{expand}(\eta_1(x),z) = \eta_1(x,z)$$
$$\mathrm{expand}(\eta_2(y),z) = \eta_2(y,z)$$

Proof. We'll first construct the map, then prove uniqueness. Since the existence of such a function cannot be assumed directly from the definition of a coproduct, let us instead define $$e : X+Y \rightarrow [Z, X\times Z + Y\times Z]$$
as follows:
$$e(\eta_1(x)) = (z \mapsto \eta_1(x,z))$$
$$e(\eta_2(y)) = (z \mapsto \eta_2(y,z))$$
Now let $\mathrm{expand} = \mathrm{uncurry}(e)$. We compute: $$\mathrm{expand}(\eta_1(x),z) = e(\eta_1(x))(z) = (z \mapsto \eta_1(x,z))(z) = \eta_1(x,z)$$
$$\mathrm{expand}(\eta_2(y),z) = e(\eta_2(y))(z) = (z \mapsto \eta_2(y,z))(z) = \eta_2(y,z)$$
To see that the constructed map is unique with respect to the desired properties, observe that those properties guarantee that $\mathrm{expand}$ is an inverse mapping to $\mathrm{factorize}$. Thus since inverses are unique, we deduce that there only one map $\mathrm{expand}$ satisfying the aforementioned equations.
