Implication Details

Claim: A category has finite products if and only if it has binary products and has a terminal object.

Proof: 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}.

This implication has a dual.

Show 124 categories using this implication