Cartesian Closed Categories

In Set, a function of two variables $f:S\times T\to V$ can be traded for a function of one variable whose values are themselves functions. Fix the first argument $s$ and what remains, $t\mapsto f(s,t)$, is a function $T\to V$. Letting $s$ vary produces a single function

where $[T\to V]$ is the set of all functions from $T$ to $V$. The passage from $f$ to $\lambda f$ is called currying $f$. It is reversible: a function $g:S\to [T\to V]$ induces $f(s,t)=[g(s)](t)$, and the two operations are mutually inverse. In one line, currying is a bijection of hom-sets,

natural in every variable.¹ A cartesian closed category is a category in which this bijection is available for all objects, with an object $[A\to B]$ standing in for the set of functions and an arrow $\mathrm{eval}$ standing in for the operation of applying a function to an argument.

The definition

A cartesian closed category has a terminal object, all binary products, and an exponential object whose evaluation arrow satisfies a universal property.

By Proposition 5.3.10 on finite products, CCC-1 and CCC-2 together say that $\mathcal{C}$ has all finite products, the terminal object being the empty product. So a cartesian closed category is a category with finite products plus exponentials.²

The exponential is traditionally written $B^A$ rather than $[A\to B]$, with $A$ called the exponent. The notation is faithful to the finite case: in $\mathbf{Set}$, if $n=\{0,1,\dots ,n-1\}$ then $B^n$ is the set of $n$-tuples of elements of $B$, i.e. the functions $n\to B$. There is a distinct arrow ${\mathrm{eval}}_B^A:[A\to B]\times A\to B$ for each pair $A,B$; the subscript and superscript are dropped when the objects are clear. The arrow $\lambda f$ is called the adjoint transpose or the curry of $f$.

Here $\overline{f}$ denotes $\lambda f$ (the adjoint transpose), and $\overline{f}\times A$ is the product of $\overline{f}$ with the identity on $A$. CCC-3 says that every arrow out of a product $C\times A$ factors uniquely through evaluation once its first factor has been curried.

Currying is a bijection

The uniqueness clause of CCC-3 says exactly that

is a bijection: every $f:C\times A\to B$ has one and only one transpose $\lambda f$, and conversely every $g:C\to [A\to B]$ un-curries to $\mathrm{eval}\circ (g\times A):C\times A\to B$. The two directions invert each other.

Taking $C=1$ specializes the bijection to $\mathrm{Hom}(A,B)\cong \mathrm{Hom}(1,[A\to B])$, since $1\times A\cong A$. The right-hand side is the set of global elements of the exponential. So the points of $[A\to B]$ correspond exactly to the arrows $A\to B$: the exponential internalizes the hom-set as an object.

Evaluation as a universal element

The bijection is natural, and the source of that naturality is a single universal element. Fix $A$ and $B$ and let $F_{A,B}=\mathrm{Hom}(-\times A,B)$ be the contravariant functor sending an object $C$ to $\mathrm{Hom}(C\times A,B)$ and an arrow $g:D\to C$ to precomposition with $g\times A$.

A universal element represents a functor, and representing objects are unique up to unique isomorphism. This forces the cartesian closed structure to be essentially unique.³

A category with finite products can be made cartesian closed in at most one way. This is the special case for exponentials of the general fact that adjoints are unique.

The product-exponential adjunction

Naturality in the second variable upgrades the same statement into an adjunction. For a fixed object $A$, the operation $[A\to -]$ extends to a functor $\mathcal{C}\to \mathcal{C}$: on an arrow $f:B\to C$ it acts by

This is one of the two internal hom functors; the other, $[-\to C]$, is contravariant and acts by precomposition inside the exponential.⁴ With these the hom-set bijection becomes natural in all three variables, and the statement becomes an adjunction.

Because it is a right adjoint, $[A\to -]$preserves limits; this is the source of the exponential laws collected below. Because $A\times -$ is a left adjoint it preserves colimits, which is why a cartesian closed category with finite sums is automatically distributive: $A\times (B+C)\cong (A\times B)+(A\times C)$.

Examples

The definition holds across quite different mathematics, with the exponential in each case the object that represents arrows from $A$.

• Set. The first example. $[A\to B]$ is the set of all functions $A\to B$, which is ${\mathrm{Hom}}_{\mathbf{Set}}(A,B)$, and $\mathrm{eval}$ is the apply map $(f,a)\mapsto f(a)$.
• Heyting algebras. A poset seen as a thin category is cartesian closed exactly when it is a Heyting algebra. Meet gives products, the top element is terminal, and the exponential $[a\to b]$ is the largest $c$ with $c\wedge a\le b$, the relative pseudocomplement, read as intuitionistic implication. Heyting algebras stand to intuitionistic logic as Boolean algebras stand to classical logic.
• Boolean algebras. The special case with $\neg \neg a=a$, where implication is $[a\to b]=\neg a\vee b$. Reading the exponential laws off a Boolean algebra yields the tautologies of classical propositional logic.
• Functor categories. For a small category $\mathcal{D}$, the category $\mathrm{Func}(\mathcal{D},\mathbf{Set})$ of set-valued functors and natural transformations is cartesian closed. Products are pointwise; the exponential $[F\to G]$ has value at $C$ the set of natural transformations $\mathrm{Hom}(C,-)\times F\to G$.
• Cat. The category of small categories and functors is cartesian closed. For categories $\mathcal{C},\mathcal{D}$ the exponential $[\mathcal{C}\to \mathcal{D}]$ is the functor category: its objects are functors and its arrows are natural transformations.
• Domains. The category of $\omega$-CPOs (countably directed-complete posets) and continuous functions is cartesian closed. This is what makes it a candidate for programming-language semantics; the fixed-point lesson returns to it.

First-class functions and modus ponens

When a functional programming language is presented as a category (types as objects, programs as arrows) and that category is cartesian closed, every pair of types $A,B$ yields a type $[A\to B]$. Since $[A\to B]$ is itself a type, programs may take it as input and produce it as output: functions become data on the same footing as everything else. This is the categorical content of the slogan that functions are first-class objects. The uniqueness proposition adds a constraint: if the function type must satisfy the currying law, there is essentially one way to build it.

When a deduction system is a cartesian closed category, the exponential turns into implication. Read $[A\to B]$ as the formula $A$ implies $B$. Then evaluation $\mathrm{eval}:[A\to B]\times A\to B$ is a proof of $B$ from $A$ and $A\Rightarrow B$, i.e. modus ponens. Currying an arrow $f:C\times A\to B$, a proof of $B$ from $C$ and $A$, produces $\lambda f:C\to [A\to B]$, a proof of $A\Rightarrow B$ from $C$. This is the deduction (or detachment) rule of propositional logic.

The exponential laws

Because $[A\to -]$ is a right adjoint it behaves like a hom-functor, and the familiar arithmetic of exponents holds up to isomorphism. Writing $B^A$ for $[A\to B]$ makes the pattern unmistakable.

The third row is currying stated as an object isomorphism: an arrow of two arguments is the same as a curried arrow of one. Each isomorphism is natural in every variable, and each can be proved by evaluating both sides against the Yoneda embedding. For the third row, for fixed $B$ and $C$,

and fullness of Yoneda promotes the natural isomorphism of representables to an isomorphism of the representing objects.⁵ Rewritten as rules of inference under the implication reading, the same table lists tautologies of propositional logic: $C^{A\times B}\cong (C^B{)}^A$ is the equivalence of $(A\wedge B)\Rightarrow C$ with $A\Rightarrow (B\Rightarrow C)$, and $C^{A+B}\cong C^A\times C^B$ is reasoning by cases.

A cartesian closed category carries three readings at once: a calculus of functions of several variables, a fragment of intuitionistic propositional logic, and a model of typed programs. That these are one structure is the Curry–Howard–Lambek correspondence — propositions correspond to types correspond to objects, and proofs to terms to arrows. The typed lambda calculus makes the programs reading exact, matching a term to each arrow.