Closed Categories

A closed category is a symmetric monoidal category where each functor has a specified right adjoint called an “exponential”: . By what we said yesterday, this means that there is a unique way to sew all these adjoints parametrized by 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 we need an adjunction . That is, functions taking a pair of elements — one from and one from — to an element of should be in bijection with functions from to . And indeed we have such an adjunction: is the set of all functions from to .

Let’s say this a bit more concretely. If we consider the set of natural numbers we have the function , which takes two numbers and gives back a third: if we stick in and we get back . 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 we get back the function . That is, we can see addition either as a function taking a pair of numbers to a number, or we can see it as a function , taking a number to a function from numbers to numbers.

More generally, if we can define , which is defined by . That is, takes an element of and gives back a function from to . 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 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 whose objects are well-formed formulas in the calculus, and whose arrows are proofs. The product in this category is , read “and”. If we know then we can derive and we can derive , so there are two arrows. On the other hand, if implies both and , then implies . This is just a rough sketch that is the categorical product, but it’s good enough for now.

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

Now if implies we have (by definition) a proof starting from and ending with . Then we can use this proof to devise a proof starting from and ending with . That is, implies if and only if implies . This shows that is right adjoint to , as we claimed.