product for free

Hi, In lambda-calculus one can define the product of types A and B by: forall C, (A->B->C)->C. with pairing and projections defined as: pair ≡ λx.λy.λz.z x y fst ≡ λp.p (λx.λy.x) snd ≡ λp.p (λx.λy.y) What would be the equivalent in a closed monoidal category? Would we get a product for free? [For admin and other information see: http://www.mta.ca/~cat-dist/ ]