CatDat

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

Show 88 categories using this implication