Re: product for free

Remark: as far as I remember, one need to be cautios calling this a product, because ordinary product equations do not hold with this definition and standard equality of lambda-calculus. Best wishes Sergei Soloviev

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/ ]