Dear David, If you consider not only a closed monoidal category, but a full model of dual intuitionistic linear logic (DILL) with parametric polymorphism, the answer is yes. A model of DILL means among other things that the tensor is symmetric, and that there is a comonad, usually denoted ! . Writing --o for the closed structure and --> for the Girard encoding A --> B = !A --o B, then one can first encode coproducts as A + B = forall C . (A --o C) --> (B --o C) --> C and then products as A x B = forall C . ((A --o C) + (B --o C)) --o C Further details on these encodings can be found in Linear Abadi and Plotkin Logic, by Birkedal, Møgelberg and Petersen, Logical methods in Computer Science, 2(5). Rasmus On 17 August 2010 15:27, David Leduc <david.leduc6@googlemail.com> wrote:
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/ ]