Cartesian closed category

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

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