More to the point, it is a "weak product" (lacking the uniqueness condition one usually has) - I think this is discussed in Lambek Scott, but am away from my library to verify this ... -= rags =- On Wed, 18 Aug 2010, soloviev@irit.fr wrote:
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/ ]