Implication Details

Assumptions: preserves binary products, preserves terminal objects

Requirements of the source: finite products

Conclusions: preserves finite products

This is an equivalence.

Proof: This is because finite products can be constructed recursively via X1×⋯×Xn+1=(X1×⋯×Xn)×Xn+1X_1 \times \cdots \times X_{n+1} = (X_1 \times \cdots \times X_n) \times X_{n+1}. We need the assumption on the source category since otherwise X1×⋯×XnX_1 \times \cdots \times X_n might not exist.