David, this is a lazy reply - I did not check anything out. One would be working with a second-order linear lambda calculus, presumably, so only the definition below of "pair" works. If one made a suitable "cut-down" version of Rasmus et al's paper, with parametricity, I would expect that, with your definition, one gets a tensor product adjoint to the function space. I don't have an immediate guess as to what one gets without parametricity. Gordon On Tue, Aug 17, 2010 at 2:27 PM, 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/ ]