In cartesian closed categories, a "function of two variables" (a morphism f:X×Y → Z) can always be represented as a "function of one variable" (the morphism λf:X → ZY). In computer science applications, this is known as currying; it has led to the realization that simply-typed lambda calculus can be interpreted in any cartesian closed category.
Certain cartesian closed categories, the topoi, have been proposed as a general s ...
Examples of cartesian closed categories include:
The category Set of all sets, with functions as morphisms, is cartesian closed. The product X×Y is the cartesian product of X and Y, and ZY is the set of all functions from Y to Z. The adjointness is expressed by the following fact: the function f : X×Y → Z is naturally identified with the function g : X → ZY defined by gSee also:
The category C is called cartesian closed iff it satisfies the following three properties:
it has a terminal object
any two objects X and Y of C have a product X×Y in C
any two objects Y and Z of C have an exponential ZY in C
For the first two conditions above, it is the same to require that any finite (possibly empty) family of objects of C admit a product in C, because of t ...
