Cartesian closed category

Last updated

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 both X 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.

The renowned 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. 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: [7]

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 additive inverses:

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. [8]

Related Research Articles

In mathematics and computer science, currying is the technique of converting a function that takes multiple arguments into a sequence of functions that each takes a single argument. For example, currying a function that takes three arguments creates three functions:

In mathematics, specifically category theory, a functor is a mapping between categories. Functors were first considered in algebraic topology, where algebraic objects are associated to topological spaces, and maps between these algebraic objects are associated to continuous maps between spaces. Nowadays, functors are used throughout modern mathematics to relate various categories. Thus, functors are important in all areas within mathematics to which category theory is applied.

In mathematics, especially in category theory and homotopy theory, a groupoid generalises the notion of group in several equivalent ways. A groupoid can be seen as a:

Universal property Central object of study in category theory

In category theory, a branch of mathematics, a universal property is an important property which is satisfied by a universal morphism. Universal morphisms can also be thought of more abstractly as initial or terminal objects of a comma category. Universal properties occur almost everywhere in mathematics, and hence the precise category theoretic concept helps point out similarities between different branches of mathematics, some of which may even seem unrelated.

In mathematics, the Yoneda lemma is arguably the most important result in category theory. It is an abstract result on functors of the type morphisms into a fixed object. It is a vast generalisation of Cayley's theorem from group theory. It allows the embedding of any locally small category into a category of functors defined on that category. It also clarifies how the embedded category, of representable functors and their natural transformations, relates to the other objects in the larger functor category. It is an important tool that underlies several modern developments in algebraic geometry and representation theory. It is named after Nobuo Yoneda.

In category theory, a branch of mathematics, the abstract notion of a limit captures the essential properties of universal constructions such as products, pullbacks and inverse limits. The dual notion of a colimit generalizes constructions such as disjoint unions, direct sums, coproducts, pushouts and direct limits.

In mathematics, specifically category theory, adjunction is a relationship that two functors may have. Two functors that stand in this relationship are known as adjoint functors, one being the left adjoint and the other the right adjoint. Pairs of adjoint functors are ubiquitous in mathematics and often arise from constructions of "optimal solutions" to certain problems, such as the construction of a free group on a set in algebra, or the construction of the Stone–Čech compactification of a topological space in topology.

In mathematics, specifically in category theory, a pre-abelian category is an additive category that has all kernels and cokernels.

In category theory, the product of two objects in a category is a notion designed to capture the essence behind constructions in other areas of mathematics such as the Cartesian product of sets, the direct product of groups or rings, and the product of topological spaces. Essentially, the product of a family of objects is the "most general" object which admits a morphism to each of the given objects.

In mathematics, the Ext functors are the derived functors of the Hom functor. Along with the Tor functor, Ext is one of the core concepts of homological algebra, in which ideas from algebraic topology are used to define invariants of algebraic structures. The cohomology of groups, Lie algebras, and associative algebras can all be defined in terms of Ext. The name comes from the fact that the first Ext group Ext1 classifies extensions of one module by another.

In mathematics, particularly category theory, a representable functor is a certain functor from an arbitrary category into the category of sets. Such functors give representations of an abstract category in terms of known structures allowing one to utilize, as much as possible, knowledge about the category of sets in other settings.

In mathematics, especially in category theory, a closed monoidal category is a category that is both a monoidal category and a closed category in such a way that the structures are compatible.

In mathematics, specifically in category theory, the category of small categories, denoted by Cat, is the category whose objects are all small categories and whose morphisms are functors between categories. Cat may actually be regarded as a 2-category with natural transformations serving as 2-morphisms.

Fibred categories are abstract entities in mathematics used to provide a general framework for descent theory. They formalise the various situations in geometry and algebra in which inverse images of objects such as vector bundles can be defined. As an example, for each topological space there is the category of vector bundles on the space, and for every continuous map from a topological space X to another topological space Y is associated the pullback functor taking bundles on Y to bundles on X. Fibred categories formalise the system consisting of these categories and inverse image functors. Similar setups appear in various guises in mathematics, in particular in algebraic geometry, which is the context in which fibred categories originally appeared. Fibered categories are used to define stacks, which are fibered categories with "descent". Fibrations also play an important role in categorical semantics of type theory, and in particular that of dependent type theories.

In mathematics, specifically in category theory, an exponential object or map object is the categorical generalization of a function space in set theory. Categories with all finite products and exponential objects are called cartesian closed categories. Categories without adjoined products may still have an exponential law.

This is a glossary of properties and concepts in category theory in mathematics.

In mathematics, specifically in category theory, hom-sets, i.e. sets of morphisms between objects, give rise to important functors to the category of sets. These functors are called hom-functors and have numerous applications in category theory and other branches of mathematics.

In category theory, a branch of mathematics, a presheaf on a category is a functor . If is the poset of open sets in a topological space, interpreted as a category, then one recovers the usual notion of presheaf on a topological space.

In mathematics, a topos is a category that behaves like the category of sheaves of sets on a topological space. Topoi behave much like the category of sets and possess a notion of localization; they are a direct generalization of point-set topology. The Grothendieck topoi find applications in algebraic geometry; the more general elementary topoi are used in logic.

In mathematics, Grothendieck's six operations, named after Alexander Grothendieck, is a formalism in homological algebra. It originally sprang from the relations in étale cohomology that arise from a morphism of schemes f : XY. The basic insight was that many of the elementary facts relating cohomology on X and Y were formal consequences of a small number of axioms. These axioms hold in many cases completely unrelated to the original context, and therefore the formal consequences also hold. The six operations formalism has since been shown to apply to contexts such as D-modules on algebraic varieties, sheaves on locally compact topological spaces, and motives.


  1. John C. Baez and Mike Stay, "Physics, Topology, Logic and Computation: A Rosetta Stone", (2009) ArXiv 0903.0340 in New Structures for Physics, ed. Bob Coecke, Lecture Notes in Physics vol. 813, Springer, Berlin, 2011, pp. 95-174.
  2. Saunders., Mac Lane (1978). Categories for the Working Mathematician (Second ed.). New York, NY: Springer New York. ISBN   1441931236. OCLC   851741862.
  3. "cartesian closed category in nLab". Retrieved 2017-09-17.
  4. Locally cartesian closed category in nLab
  5. H. P. Barendregt, The Lambda Calculus, (1984) North-Holland ISBN   0-444-87508-5 (See theorem 1.2.16)
  6. "Ct.category theory - is the category commutative monoids cartesian closed?".
  7. S. Soloviev. "Category of Finite Sets and Cartesian Closed Categories", Journal of Soviet Mathematics, 22, 3 (1983)
  8. Fiore, Cosmo, and Balat. Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types