Implication Details

Claim: Given a functor whose domain has finite products, if it preserves binary products and preserves terminal objects, then it preserves finite products.

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 domain since otherwise X1×⋯×XnX_1 \times \cdots \times X_n might not exist. See MSE/5142961.