---
title: Cartesian Closed Categories
module: Cartesian Closed Categories and Typed Lambda Calculus
moduleNumber: 8
lessonNumber: 1
order: 801
summary: >
  A cartesian closed category has a terminal object, binary products, and for
  every pair of objects an exponential object that internalizes the hom-set as
  an object of the category. The defining data is an evaluation arrow and a
  currying operation, packaged by the adjunction between product-with-A and
  exponential-by-A. Set, Boolean and Heyting algebras, functor categories, and
  Cat are all cartesian closed.
topics: [Cartesian Closed Categories and Typed Lambda Calculus]
sources:
  - book: Barr & Wells
    ref: "Ch. 6 — Cartesian closed categories; §6.1 Cartesian closed categories"
  - book: Barr & Wells
    ref: "§6.2 Properties of cartesian closed categories"
draft: false
---

In [Set](/category-theory/foundations/examples-of-categories), 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

$$
\lambda f : S \longrightarrow [T \to V], \qquad (\lambda f)(s) = \bigl(t \mapsto f(s,t)\bigr),
$$

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,

$$
\mathrm{Hom}_{\mathbf{Set}}(S \times T,\; V) \;\cong\; \mathrm{Hom}_{\mathbf{Set}}\bigl(S,\; [T \to V]\bigr),
$$

natural in every variable.[^bw-curry] 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.

> **Definition (Cartesian closed category).** A category $\mathcal{C}$ is
> **cartesian closed** (a CCC) if it satisfies:
>
> - **CCC-1.** There is a terminal object $1$.
> - **CCC-2.** Each pair of objects $A, B$ has a product $A \times B$ with
>   projections $p_1 : A \times B \to A$ and $p_2 : A \times B \to B$.
> - **CCC-3.** For every pair $A, B$ there is an object $[A \to B]$ and an arrow
>   $\mathrm{eval} : [A \to B] \times A \to B$ such that for every arrow
>   $f : C \times A \to B$ there is a **unique** arrow
>   $\lambda f : C \to [A \to B]$ making
>   $\mathrm{eval} \circ (\lambda f \times A) = f$.

By [Proposition 5.3.10 on finite products](/category-theory/universal-properties/products-and-coproducts),
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.[^bw-ccc]

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}^A_B : [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$.

$$
% caption: The exponential universal property: eval applied after currying $f$ (in its first factor) recovers $f$, and $\overline{f}$ is the only arrow that does this.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\node (ca) at (0,2.2) {$C \times A$};
\node (ea) at (0,0) {$B^A \times A$};
\node (b)  at (4.2,0) {$B$};
\draw[->, acc, thick] (ca) -- (ea) node[midway, left, black] {$\overline{f} \times A$};
\draw[->, thick] (ea) -- (b) node[midway, below, black] {$\mathrm{ev}$};
\draw[->, acc, thick] (ca) -- (b) node[midway, above right, black] {$f$};
\end{tikzpicture}
$$

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

$$
\lambda : \mathrm{Hom}(C \times A,\; B) \;\longrightarrow\; \mathrm{Hom}\bigl(C,\; [A \to B]\bigr)
$$

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.

$$
% caption: Currying and its inverse exchange an arrow out of a product for an arrow into an exponential; the two hom-sets are in bijection for all $C$.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\node[draw, acc, thick, minimum width=34mm, minimum height=11mm] (l) at (0,0) {arrows $C \times A$ to $B$};
\node[draw, thick, minimum width=34mm, minimum height=11mm] (r) at (6.6,0) {arrows $C$ to $B^A$};
\draw[->, acc, thick] (l.north east) to[bend left=22] node[midway, above, black] {curry} (r.north west);
\draw[->, thick] (r.south west) to[bend left=22] node[midway, below, black] {uncurry} (l.south east);
\end{tikzpicture}
$$

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.

> **Worked example (Counting an exponential in Set).** Take $A = \{0, 1\}$ and
> $B = \{r, g, b\}$. The exponential $[A \to B] = B^A$ is the set of functions
> $A \to B$; a function is fixed by its two values, so
> $$
> \lvert B^A\rvert = \lvert B\rvert^{\lvert A\rvert} = 3^2 = 9,
> $$
> the nine pairs $(f(0), f(1)) \in B \times B$. Evaluation
> $\mathrm{eval} : B^A \times A \to B$ has $9 \times 2 = 18$ argument pairs and
> sends $(f, a) \mapsto f(a)$; for the function $f$ with $f(0) = r$ and
> $f(1) = g$ it gives $\mathrm{eval}(f, 0) = r$ and $\mathrm{eval}(f, 1) = g$.
> Setting $C = 1$ in the currying bijection reads
> $$
> \mathrm{Hom}(A, B) \cong \mathrm{Hom}(1, B^A),
> $$
> both sides of size $9$: an arrow $A \to B$ on the left, a global element of
> $B^A$ on the right. For a general $h : C \times A \to B$ with $\lvert C\rvert =
> c$, currying matches $\lvert B\rvert^{\lvert C \times A\rvert} = 3^{2c}$ arrows
> against $(\lvert B\rvert^{\lvert A\rvert})^{c} = 9^{c} = 3^{2c}$ transposes, so
> the counts agree for every $c$.

### 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$.

> **Proposition (Evaluation as a universal element).** In a cartesian closed
> category, $\mathrm{eval} : [A \to B] \times A \to B$ is a
> [universal element](/category-theory/representables-yoneda/representable-functors)
> for $F_{A,B} = \mathrm{Hom}(- \times A, B)$. Consequently $f \mapsto \lambda f$
> is a natural isomorphism of functors
> $$
> \mathrm{Hom}(- \times A,\; B) \;\cong\; \mathrm{Hom}\bigl(-,\; [A \to B]\bigr).
> $$

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.[^bw-uniq]

> **Proposition (Uniqueness of the structure).** Let $\mathcal{C}$ have finite
> products. If $[A \to B]$ with $\mathrm{eval}$ and $[A \to B]'$ with
> $\mathrm{eval}'$ both satisfy CCC-3, then there is a unique isomorphism
> $\varphi(A,B) : [A \to B]' \to [A \to B]$ compatible with both evaluation
> arrows and both currying operations.

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](/category-theory/adjunctions/adjunctions).

## 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

$$
[A \to f] \;=\; \lambda\bigl(f \circ \mathrm{eval}\bigr) : [A \to B] \longrightarrow [A \to C].
$$

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

> **Theorem (Product-exponential adjunction).** In a cartesian closed category,
> for each object $A$ the functor $A \times -$ is left adjoint to $[A \to -]$:
> $$
> \mathrm{Hom}(A \times C,\; B) \;\cong\; \mathrm{Hom}\bigl(C,\; [A \to B]\bigr),
> \qquad \text{natural in } B \text{ and } C.
> $$
> Currying is the adjunction's hom-set bijection; evaluation is its counit.

$$
% caption: Product-with-$A$ is left adjoint to exponential-by-$A$; currying moves an arrow across the adjunction and evaluation is the counit at $B$.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\node (c) at (0,0) {$\mathcal{C}$};
\node (d) at (5,0) {$\mathcal{C}$};
\draw[->, acc, thick] (c) to[bend left=28] node[midway, above, black] {product with $A$ (left adjoint)} (d);
\draw[->, thick] (d) to[bend left=28] node[midway, below, black] {exponential by $A$ (right adjoint)} (c);
\end{tikzpicture}
$$

Because it is a right adjoint, $[A \to -]$
[preserves limits](/category-theory/adjoints-limits/adjoints-preserve-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](/category-theory/foundations/examples-of-categories)
  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](/category-theory/foundations/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](/category-theory/foundations/natural-transformations): 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](/category-theory/cartesian-closed-lambda/fixed-points-and-recursion)
  returns to it.

> **Worked example (Exponentials in a Boolean algebra).** In a Boolean algebra
> read as a thin category, products are meets, so CCC-3 asks for an element
> $[a \to b]$ with $[a \to b] \wedge a \le b$ and with $c \wedge a \le b$ implying
> $c \le [a \to b]$. Take $[a \to b] = \neg a \vee b$. Evaluation exists because,
> by distributivity,
> $$
> (\neg a \vee b) \wedge a = (\neg a \wedge a) \vee (b \wedge a) = 0 \vee (b \wedge a) = b \wedge a \le b.
> $$
> Currying exists because, assuming $c \wedge a \le b$,
> $$
> c = c \wedge (a \vee \neg a) = (c \wedge a) \vee (c \wedge \neg a) \le b \vee \neg a = \neg a \vee b = [a \to b].
> $$
> Uniqueness and the equation $\mathrm{eval} \circ (\lambda f \times A) = f$ are
> automatic: no hom-set in a poset-category has more than one element.

### First-class functions and modus ponens

When a [functional programming language is presented as a category](/category-theory/foundations/examples-of-categories)
(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.

$$
% caption: In a deduction system that is a CCC, evaluation is modus ponens: from a proof of $A$ and a proof of $A$ implies $B$ it produces a proof of $B$.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\node (imp) at (0,1.4) {$B^A$};
\node (a)   at (2.6,1.4) {$A$};
\node (prod) at (1.3,0.2) {$B^A \times A$};
\node (b)   at (1.3,-1.4) {$B$};
\draw[->, thick] (imp) -- (prod);
\draw[->, thick] (a) -- (prod);
\draw[->, acc, thick] (prod) -- (b) node[midway, right, black] {$\mathrm{ev}$};
\end{tikzpicture}
$$

## 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.

| Isomorphism (bracket form) | Exponential form | Condition |
| --- | --- | --- |
| $[A \to 1] \cong 1$ | $1^A \cong 1$ | always |
| $[1 \to A] \cong A$ | $A^1 \cong A$ | always |
| $[A \times B \to C] \cong [A \to [B \to C]]$ | $C^{A \times B} \cong (C^B)^A$ | always |
| $[A \to B] \times [A \to C] \cong [A \to B \times C]$ | $B^A \times C^A \cong (B \times C)^A$ | always |
| $[0 \to A] \cong 1$ | $A^0 \cong 1$ | needs initial object $0$ |
| $[A + B \to C] \cong [A \to C] \times [B \to C]$ | $C^{A+B} \cong C^A \times C^B$ | needs sum $A + B$ |

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](/category-theory/representables-yoneda/yoneda-consequences).
For the third row, for fixed $B$ and $C$,

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

and fullness of Yoneda promotes the natural isomorphism of representables to an
isomorphism of the representing objects.[^bw-laws] 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](/category-theory/cartesian-closed-lambda/lambda-calculus-correspondence)
makes the programs reading exact, matching a term to each arrow.

[^bw-curry]: **Barr & Wells**, _Category Theory for Computing Science_, §6.1.2 — currying a function of two variables and the resulting hom-set isomorphism $\mathrm{Hom}(S \times T, V) \cong \mathrm{Hom}(S, [T \to V])$.
[^bw-ccc]: **Barr & Wells**, §6.1.3–6.1.5 — the definition CCC-1 through CCC-3, the notation $B^A$ for the exponential, and the reduction of CCC-1/CCC-2 to the existence of finite products.
[^bw-uniq]: **Barr & Wells**, §6.1.7–6.1.8 — evaluation as a universal element for $\mathrm{Hom}(- \times A, B)$, and the resulting uniqueness of the cartesian closed structure up to unique isomorphism.
[^bw-inthom]: **Barr & Wells**, §6.2.1–6.2.3 — the internal hom functors $[A \to -]$ and $[- \to C]$, and the restatement of CCC-3 as the adjunction $A \times - \dashv [A \to -]$; distributivity in §6.2.3.
[^bw-laws]: **Barr & Wells**, §6.2.4 — the six exponential isomorphisms and the proof of $[A \times B \to C] \cong [A \to [B \to C]]$ by fullness of the Yoneda embedding.