Implication Details

Assumptions: finite products

Conclusions: binary products, terminal object

This is an equivalence.

Reason: The non-trivial direction follows since 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}.