# The Unapologetic Mathematician

## Closed Categories

A closed category is a symmetric monoidal category $\mathcal{C}$ where each functor $\underline{\hphantom{X}}\otimes B$ has a specified right adjoint called an “exponential”: $(\underline{\hphantom{X}})^B$. By what we said yesterday, this means that there is a unique way to sew all these adjoints parametrized by $\mathcal{C}$ together into a functor.

The canonical example of such a category is the category of sets with the cartesian product as its monoidal structure. For each set $B$ we need an adjunction $\hom_\mathbf{Set}(A\times B,C)\cong\hom_\mathbf{Set}(A,C^B)$. That is, functions taking a pair of elements — one from $A$ and one from $B$ — to an element of $C$ should be in bijection with functions from $A$ to $C^B$. And indeed we have such an adjunction: $C^B$ is the set $\hom_\mathbf{Set}(B,C)$ of all functions from $B$ to $C$.

Let’s say this a bit more concretely. If we consider the set of natural numbers $\mathbb{N}$ we have the function $+$, which takes two numbers and gives back a third: if we stick in $1$ and $2$ we get back $1+2=3$. But what if we just stick in the first number of the pair? Then what we get back is a function that will take the second number and give us the sum: if we just feed in $1$ we get back the function $x\mapsto1+x$. That is, we can see addition either as a function $\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ taking a pair of numbers to a number, or we can see it as a function $\mathbb{N}\rightarrow\mathbb{N}^\mathbb{N}$, taking a number to a function from numbers to numbers.

More generally, if $f:A\times B\rightarrow C$ we can define $\bar{f}(a)=f_a$, which is defined by $f_a(b)=f(a,b)\in C$. That is, $\bar{f}$ takes an element of $A$ and gives back a function from $B$ to $C$. We call this process of turning functions of many variables into functions of a single variable at a time “currying”, after Haskell Curry. It turns out to be phenomenally useful for discussing theories of computation, and forms part of the basis of functional programming.

Closed categories are an attempt to mirror this currying procedure in other categories. In general, if the monoidal structure in question is the categorical product (which is always symmetric) then we say the category is “cartesian closed”. Most such categories still look a lot like this example in sets, with morphisms given by functions preserving structure and the exponential given by an appropriate analogue of the $\hom$ functor.

Here’s an example, though, of a cartesian closed category that looks rather different. It requires the notion of a “predicate calculus”, but not very much of it. Basically, if you have a rough idea of what such a thing is you’ll be fine.

Okay, there’s a category $\mathcal{F}$ whose objects are well-formed formulas in the calculus, and whose arrows are proofs. The product in this category is $\wedge$, read “and”. If we know $P\wedge Q$ then we can derive $P$ and we can derive $Q$, so there are two arrows. On the other hand, if $R$ implies both $P$ and $Q$, then $R$ implies $P\wedge Q$. This is just a rough sketch that $\wedge$ is the categorical product, but it’s good enough for now.

Anyhow, the exponential is $\implies$, read “implies”. This is subtler than it seems. In the last paragraph I was saying things like “$P$ implies $Q$“, but this is not what I mean here. The formula $P\implies Q$ is the statement within the calculus that there exists a proof starting from $P$ and ending with $Q$. Writing out “implies” as I’m discussing the structure is a high-level view from outside the system. Writing $\implies$ in the structure itself is a low-level view, “internal” to the category. “$P$ implies $Q$” is a statement about the category, while “$P\implies Q$” is a statement within the category.

Now if $P\wedge Q$ implies $R$ we have (by definition) a proof starting from $P\wedge Q$ and ending with $R$. Then we can use this proof to devise a proof starting from $P$ and ending with $Q\implies R$. That is, $P\wedge Q$ implies $R$ if and only if $P$ implies $Q\implies R$. This shows that $Q\implies\underline{\hphantom{X}}$ is right adjoint to $P\wedge\underline{\hphantom{X}}$, as we claimed.