**Cartesian closed category** - a category that allows currying , that is, containing for each class of morphisms$A\to B$ some object$A\Rightarrow B$ 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 .

## Content

## Definition

A category *C* is called **Cartesian closed** ^{[1]} 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.

## Application

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$\lambda$ 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 .

## Notes

- ↑
*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 .

## Literature

*Curien P.-L.*Categorical combinatory logic .-- LNCS, 194, 1985, pp. ~ 139-151.*Roy L. Crole*, Categories for Types, Cambridge University Press, 1994.