Cartesian closed category - a category that allows currying , that is, containing for each class of morphisms some object representing him. Cartesian closed categories occupy, in a sense, an intermediate position between abstract categories and sets , since they allow you to correctly operate with functions , but do not allow, for example, to operate with subobjects.
From a programming point of view , Cartesian closed categories implement the encapsulation of function arguments — each argument is represented by a category object and is used as a black box . At the same time, the expressiveness of Cartesian closed categories is quite enough to operate with functions in the manner adopted in the λ-calculus . This makes them natural categorical models of typed λ-calculus .
A category C is called Cartesian closed  if it satisfies three conditions:
- C has a terminal object ;
- any two objects X , Y in C have the product X × Y ;
- any two objects Y , Z in C have exponential Z Y.
A category such that for any of its objects the category of objects above it is Cartesian closed is called locally Cartesian closed .
Examples of Cartesian closed categories
- The category of sets naturally represents a Cartesian closed category, since functions from one set to another are a set, and therefore an object. Also in it there are works ( Cartesian works ) and terminal objects - singletons .
- The Cat category of all small categories (and functors as morphisms) is Cartesian closed; the exponential C D is a category of functors from D to C with natural transformations as morphisms. There is also a product category and a terminal object - category 1 from one object and one morphism.
- Elementary topos is a Cartesian closed category by definition.
- Heyting algebra is also a standard example of a Cartesian closed category. Since Boolean algebra is a special case of it, it is also always Cartesian closed.
In the Cartesian closed category, the “function of two variables” (morphism f : X × Y → Z ) can always be represented as the “function of one variable” (morphism λ f : X → Z Y ). In programming, this operation is known as currying ; this allows you to interpret a simply typed lambda calculus in any Cartesian closed category. Cartesian closed categories serve as a categorical model for typed calculus and combinatorial logic .
The Curry - Howard correspondence provides an isomorphism between intuitionistic logic, simply typed lambda calculus and Cartesian closed categories. Certain Cartesian closed categories ( toposs ) were proposed as the main objects of the alternative foundations of mathematics instead of the traditional set theory .
- MacLane S. Chapter 4. Conjugate functors // Categories for the working mathematician = Categories for the working mathematician / Per. from English under the editorship of V.A. Artamonova. - M .: Fizmatlit, 2004. - S. 95-128. - 352 p. - ISBN 5-9221-0400-4 .
- Curien P.-L. Categorical combinatory logic .-- LNCS, 194, 1985, pp. ~ 139-151.
- Roy L. Crole , Categories for Types, Cambridge University Press, 1994.