CatDat

Implication Details

Claim: If a category has pullbacks and has a terminal object, then it has binary products.

Proof: If $1$ is a terminal object, then $X \times_1 Y = X \times Y$.