Implication Details

Assumptions: cartesian closed, coproducts

Conclusions: infinitary distributive

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