Main Page | See live article | Alphabetical index

Cartesian closed category

In category theory, a category is cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in logic and the theory of programming.

Table of contents
1 Definition
2 Examples
3 Applications
4 Equational theory

Definition

The category C is called cartesian closed iff it satisfies the following three properties:

The right adjoint of −×Y, applied to the object Z, is written as HOM(Y,Z), Y=>Z or ZY; we will use the exponential notation in the sequel. The adjointness condition means that the set of morphisms in C from X×Y to Z is naturally identified with the set of morphisms from X to ZY, for any three objects X, Y and Z in C.

The term "cartesian closed" is used because one thinks of Y×X as akin to the cartesian product of two sets.

Examples

Examples of cartesian closed categories include:

The following categories are not cartesian closed:

Applications

In cartesian closed categories, a "function of two variables" can always be represented as a "function of one variable". In other contexts, this is known as currying; it has lead to the realization that lambda calculus can be formulated in any cartesian closed category.

Certain cartesian closed categories, the topoi, have been proposed as a general setting for mathematics.

Equational theory

In every cartesian closed category (using exponential notation), (XY)Z and (XZ)Y are isomorphic for all objects X, Y and Z. We write this as the "equation"

(xy)z = (xz)y

What other such equations are valid in all cartesian closed categories? It turns out that all of them follow logically from the following axioms: