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 mathematical logic and the theory of programming, in that their internal language is the simply typed lambda calculus. They are generalized by closed monoidal categories, whose internal language, linear type systems, are suitable for both quantum and classical computation.[1]


Named after René Descartes (1596–1650), French philosopher, mathematician, and scientist, whose formulation of analytic geometry gave rise to the concept of Cartesian product, which was later generalized to the notion of categorical product.


The category C is called Cartesian closed[2] if and only if it satisfies the following three properties:

The first two conditions can be combined to the single requirement that any finite (possibly empty) family of objects of C admit a product in C, because of the natural associativity of the categorical product and because the empty product in a category is the terminal object of that category.

The third condition is equivalent to the requirement that the functor – ×Y (i.e. the functor from C to C that maps objects X to X ×Y and morphisms φ to φ × idY) has a right adjoint, usually denoted –Y, for all objects Y in C. For locally small categories, this can be expressed by the existence of a bijection between the hom-sets

which is natural in X, Y, and Z.[3]

Take care to note that a Cartesian closed category need not have finite limits; only finite products are guaranteed.

If a category has the property that all its slice categories are Cartesian closed, then it is called locally cartesian closed.[4] Note that if C is locally Cartesian closed, it need not actually be Cartesian closed; that happens if and only if C has a terminal object.

Basic constructions


For each object Y, the counit of the exponential adjunction is a natural transformation

called the (internal) evaluation map. More generally, we can construct the partial application map as the composite

In the particular case of the category Set, these reduce to the ordinary operations:


Evaluating the exponential in one argument at a morphism p : XY gives morphisms

corresponding to the operation of composition with p. Alternate notations for the operation pZ include p* and p∘-. Alternate notations for the operation Zp include p* and -∘p.

Evaluation maps can be chained as

the corresponding arrow under the exponential adjunction

is called the (internal) composition map.

In the particular case of the category Set, this is the ordinary composition operation:


For a morphism p:XY, suppose the following pullback square exists, which defines the subobject of XY corresponding to maps whose composite with p is the identity:

where the arrow on the right is pY and the arrow on the bottom corresponds to the identity on Y. Then ΓY(p) is called the object of sections of p. It is often abbreviated as ΓY(X).

If ΓY(p) exists for every morphism p with codomain Y, then it can be assembled into a functor ΓY : C/YC on the slice category, which is right adjoint to a variant of the product functor:

The exponential by Y can be expressed in terms of sections:


Examples of Cartesian closed categories include:

Examples of locally Cartesian closed categories include:

Non-examples of locally Cartesian closed categories include:


In Cartesian closed categories, a "function of two variables" (a morphism f : X×YZ) can always be represented as a "function of one variable" (the morphism λf : XZY). 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.

The Curry–Howard–Lambek correspondence provides a deep isomorphism between intuitionistic logic, simply-typed lambda calculus and Cartesian closed categories.

Certain Cartesian closed categories, the topoi, have been proposed as a general setting for mathematics, instead of traditional set theory.

Computer scientist John Backus has advocated a variable-free notation, or Function-level programming, which in retrospect bears some similarity to the internal language of Cartesian closed categories.[7] CAML is more consciously modelled on Cartesian closed categories.

Dependent sum and product

Let C be a locally Cartesian closed category. Then C has all pullbacks, because the pullback of two arrows with codomain Z is given by the product in C/Z.

For every arrow p : XY, let P denote the corresponding object of C/Y. Taking pullbacks along p gives a functor p* : C/YC/X which has both a left and a right adjoint.

The left adjoint is called the dependent sum and is given by composition .

The right adjoint is called the dependent product.

The exponential by P in C/Y can be expressed in terms of the dependent product by the formula .

The reason for these names is because, when interpreting P as a dependent type , the functors and correspond to the type formations and respectively.

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.

One may ask what other such equations are valid in all Cartesian closed categories. It turns out that all of them follow logically from the following axioms:[8]

Bicartesian closed categories

Bicartesian closed categories extend Cartesian closed categories with binary coproducts and an initial object, with products distributing over coproducts. Their equational theory is extended with the following axioms, yielding something similar to Tarski's high school axioms but with a zero:

Note however that the above list is not complete; type isomorphism in the free BCCC is not finitely axiomatizable, and its decidability is still an open problem.[9]


  1. ^ Baez, John C.; Stay, Mike (2011). "Physics, Topology, Logic and Computation: A Rosetta Stone" (PDF). In Coecke, Bob (ed.). New Structures for Physics. Lecture Notes in Physics. Vol. 813. Springer. pp. 95–174. arXiv:0903.0340. CiteSeerX doi:10.1007/978-3-642-12821-9_2. ISBN 978-3-642-12821-9. S2CID 115169297.
  2. ^ Saunders, Mac Lane (1978). Categories for the Working Mathematician (2nd ed.). Springer. ISBN 1441931236. OCLC 851741862.
  3. ^ "cartesian closed category in nLab". Retrieved 2017-09-17.
  4. ^ Locally cartesian closed category at the nLab
  5. ^ Barendregt, H.P. (1984). "Theorem 1.2.16". The Lambda Calculus. North-Holland. ISBN 0-444-87508-5.
  6. ^ "Ct.category theory - is the category commutative monoids cartesian closed?".
  7. ^ Backus, John (1981). Function level programs as mathematical objects. New York, New York, USA: ACM Press. doi:10.1145/800223.806757.
  8. ^ Solov'ev, S.V. (1983). "The category of finite sets and Cartesian closed categories". J Math Sci. 22 (3): 1387–1400. doi:10.1007/BF01084396. S2CID 122693163.
  9. ^ Fiore, M.; Cosmo, R. Di; Balat, V. (2006). "Remarks on isomorphisms in typed lambda calculi with empty and sum types" (PDF). Annals of Pure and Applied Logic. 141 (1–2): 35–50. doi:10.1016/j.apal.2005.09.001.