Cartesian Closed Categories — Mathematics Knowledge System

Overview

A Cartesian closed category (CCC) is a category with all finite products and exponential objects (internal hom). The exponential [B, C] (or C^B) represents the 'object of morphisms' from B to C, characterized by the natural bijection Hom(A x B, C) ~= Hom(A, [B,C]). CCCs are the categorical models of simply typed lambda calculus (Curry-Howard-Lambek correspondence). Key examples: Set (exponential = function sets), Cat (functor categories), posets with Heyting algebra structure, toposes. CCCs provide the algebraic foundation for functional programming semantics.

Intuition

In Set, for any two sets B and C, there is a set C^B = {all functions B->C}. Cartesian closed categories generalize this: the exponential object C^B (or [B,C]) represents 'functions from B to C' inside the category, even when morphisms are not literally functions. The key property: giving a morphism A x B -> C is the same as giving a morphism A -> C^B (currying). This is the categorical version of currying from functional programming: f: A x B -> C curries to f~: A -> B -> C.

Formal Definition

Definition

A category C is Cartesian closed if: (1) C has a terminal object 1; (2) any two objects have a product A x B; (3) for any two objects B, C there is an exponential object [B,C] with a natural bijection phi_{A,B,C}: Hom(A x B, C) -> Hom(A, [B,C]), natural in all three variables. The counit of the corresponding adjunction (- x B) -| [B,-] is the evaluation morphism ev: [B,C] x B -> C (apply a function to an argument).

\mathrm{Hom}(A \times B, C) \cong \mathrm{Hom}(A, [B, C])

Cartesian closed exponential

\mathrm{ev}: [B,C] \times B \to C

Evaluation morphism

(- \times B) \dashv [B, -]

Adjunction: product vs. exponential

[B, C] = C^B \text{ (exponential object)}

Exponential notation

Notation

Notation	Meaning
$[B, C]$	Exponential object (internal hom from B to C)
$C^B$	Alternative notation for exponential object
$\mathrm{ev}: C^B \times B \to C$	Evaluation morphism
$\lambda f: A \to C^B$	Curried form of f: A x B -> C

Theorems

Theorem 1: Curry-Howard-Lambek Correspondence

There is an equivalence between: (1) Types and terms of simply typed lambda calculus; (2) Propositions and proofs of intuitionistic propositional logic; (3) Objects and morphisms of a Cartesian closed category. Under this correspondence: function types A -> B correspond to exponentials [A,B]; products A x B correspond to conjunction A and B; the terminal object 1 corresponds to True. Lambda abstraction corresponds to currying; function application corresponds to evaluation.

Theorem 2: Set is Cartesian Closed

The category Set of sets and functions is Cartesian closed: products are Cartesian products A x B, the terminal object is any singleton {*}, and the exponential [B,C] = C^B is the set of all functions from B to C. The evaluation map is ev(f, b) = f(b). The adjunction Hom(A x B, C) ~= Hom(A, C^B) is the currying bijection: any function f: A x B -> C corresponds to curry(f): a -> (b -> f(a,b)).

Theorem 3: Topos is Cartesian Closed

Every topos is Cartesian closed. This follows because in a topos, finite limits exist (giving products) and the power object P(A) = Omega^A provides exponentials. The evaluation in a topos corresponds to the membership relation: for the subobject classifier Omega, [B, Omega] classifies subobjects of B.

Worked Examples

1
Given f: A x B -> C, define curry(f): A -> C^B by curry(f)(a) = (b -> f(a,b)). This maps each a in A to the function b -> f(a,b) in C^B.
2
Conversely, given g: A -> C^B, define uncurry(g): A x B -> C by uncurry(g)(a,b) = g(a)(b).
3
curry and uncurry are inverse: curry(uncurry(g))(a)(b) = uncurry(g)(a,b) = g(a)(b). And uncurry(curry(f))(a,b) = curry(f)(a)(b) = f(a,b).
4
Both maps are natural in A, B, C (functorial in each variable). So Hom(A x B, C) ~= Hom(A, C^B) naturally.
$\mathrm{Hom}(A \times B, C) \cong \mathrm{Hom}(A, C^B)$

✓ Answer

The currying bijection in Set: f <-> curry(f) via curry(f)(a)(b) = f(a,b). This is the exponential/product adjunction.

Practice Problems

Hardfree response

Explain why the category Grp of groups is NOT Cartesian closed.

Common Mistakes

Common Mistake

Thinking that every category with products is Cartesian closed.

Products and Cartesian closedness are separate conditions. Grp has all products (direct products) but is NOT Cartesian closed (no internal hom for groups). The category of topological spaces Top has products but is NOT Cartesian closed in general (the product of a compact space with a space is not always the correct topology for the function space). The convenient category of compactly generated spaces CGHaus IS Cartesian closed, which is why it's used in algebraic topology.

Quiz

In a Cartesian closed category, the exponential [B,C] satisfies:

Hom(A, [B,C]) ~= Hom(B, [A,C]) for all AHom(A x B, C) ~= Hom(A, [B,C]) naturally in A, B, C[B,C] is a product of B and CEvery morphism from B to C factors through [B,C]

Historical Background

The notion of Cartesian closed categories was developed by Lawvere in the 1960s as part of his program to provide categorical foundations for mathematics. The connection to lambda calculus was made precise by Lambek (1980), establishing the Curry-Howard-Lambek correspondence: typed lambda calculus, intuitionistic logic, and CCCs are equivalent in a precise sense. Seely (1984) extended this to dependent types. CCCs became fundamental in theoretical computer science and the semantics of functional programming languages.

1963
Lawvere introduces Cartesian closed categories in his thesis
F. William Lawvere
1980
Lambek establishes CCC as denotational semantics of typed lambda calculus
Joachim Lambek
1984
Seely extends Curry-Howard-Lambek to dependent types
R.A.G. Seely

Summary

CCC: a category with finite products and exponentials [B,C] satisfying Hom(A x B, C) ~= Hom(A, [B,C]).
Set, Cat (as 2-cat), and every topos are Cartesian closed.
Curry-Howard-Lambek: CCC = typed lambda calculus = intuitionistic logic.
Evaluation ev: [B,C] x B -> C is the counit of the product-exponential adjunction.

References

BookMac Lane, S. Categories for the Working Mathematician. 2nd ed. Springer, 1998.
BookLambek, J. and Scott, P.J. Introduction to Higher Order Categorical Logic. Cambridge, 1988.
WebsitenLab -- Cartesian closed category