Are there standard approaches to show that a non CCC category is distributive?
By the way, I know that a CCC category is distributive and I suppose that what makes the things work is that there is an exponential. But I have tried (not too hard) to prove the existence of the $(A\oplus B)\times C \rightarrow (A\times C) \oplus (B\times C)$ in a CCC category using exponentials, but I didn't succeed....any idea or pointer to an article ?
Thanks
Here is the explicit execution of "left adjoints preserve colimits":
\begin{align*} \mathrm{Hom}((A + B) \times C, D) &\cong \mathrm{Hom}(A + B, D^C) \\ &\cong \mathrm{Hom}(A, D^C) \times \mathrm{Hom}(B, D^C) \\ &\cong \mathrm{Hom}(A \times C, D) \times \mathrm{Hom}(B \times C, D) \\ &\cong \mathrm{Hom}((A \times C) + (B \times C), D) \end{align*}
Therefore, by the (covariant) Yoneda lemma, $(A + B) \times C$ is isomorphic to $(A \times C) + (B \times C)$.
The distributivity condition is equivalent to asking that the functor $(-) \times C$ preserves coproducts for all $C \in \mathscr C$. This is easy to verify abstractly for any cartesian-closed category since $(-) \times C \dashv (-)^C$ and left adjoints preserve coproducts (indeed, any colimit), as Andrej Bauer proves in their answer.
Assuming you have a concrete characterisation of the products and coproducts in your category $\mathscr C$, you may simply unwind the definitions on both sides of the equation and check the two objects are isomorphic. This is because it suffices to show that any natural isomorphism exists between $(A + B) \times C$ and $A \times C + B \times C$ to imply distributivity.
For simpler heuristics, you can check that $\mathscr C$ satisfies the properties of any distributive category, e.g. the initial object must be strict.
