Re: product for free

["Rasmus Møgelberg" <mogel@itu.dk>]

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