Implication Details

Assumptions: cartesian closed, finite coproducts

Conclusions: distributive

Reason: Each functor A×−A \times - is left adjoint and hence preserves finite coproducts (in fact, all colimits).