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

here’s hoping that your comment at michi’s

doesn’t imply that you’d rather *not* have

a link to one of your category theory posts

in the next “carnival of mathematics”.

i’m hosting august 10 … and as far as i’m

concerned, we need plenty of straight-up

university-level math to go with the highschool

stuff and the mathed. i’ll check back here

after a while to see what you think …

Comment by vlorbik | August 1, 2007 |

[...] Closed Categories A closed category is a symmetric monoidal category [LaTeX] where each functor [LaTeX] has a specified right adjoint […] [...]

Pingback by Top Posts « WordPress.com | August 3, 2007 |

Sorry, vlorbik, your comment got caught in the filter. Should be better now.

Anyhow, I’ll see if there’s anything particularly natural to post about by then, but I’ll be moving early next week and will have minimal opportunity to really put in the time to craft a suitable post for a Carnival submission. On the other hand, I can put some effort this weekend into organizing my tags a bit, so if you want to link to some subtopic of the category theory that you find particularly well-done, go right ahead.

Comment by John Armstrong | August 3, 2007 |

Actually that last example is not that different from the first one. This is (one way of viewing) the Curry-Howard correspondence (and why it’s sometimes referred to as the Curry-Howard-Lawvere or Curry-Howard-Lambek correspondence).

Comment by Derek Elkins | August 7, 2007 |

oh. okay, then. i took that for an eloquent silence.

i’ll post a link in the carnival, then. have a nice trip.

(north, south, west … wherever …)

Comment by vlorbik | August 8, 2007 |

[...] that is not only monoidal (which is needed to have an enriched category), but also symmetric and closed. Remember that “closed” means we have an adjunction for each object . In the set is [...]

Pingback by Internal Hom Functors « The Unapologetic Mathematician | August 23, 2007 |

No, I’m afraid you got the definitions all wrong.

A closed category is an axiomatization of the notion of categories with internal function space, as abstracted in the idea of “internal hom objects”. You are confusing “monoidal closed” with plain “closed”. Even logicians want to study logics with implication only as the primitive propositional connective, without assuming the internal hom has a left adjoint (given by tensor or some kind of conjunction). This was all first defined in a long article by Eilenberg and Kelly called “Closed Categories”. They even have the notion of symmetric closed, without assuming tensors at all. Of course, if you add axioms for a tensor which is adjoint to the internal hom, then you get monoidal closed categories, which are very nice. But not necessary.

Comment by Philip Scott | September 10, 2007 |

Philip, I think that our disagreement is pure language. You say “monoidal closed” where I use “closed” as a modifier for a monoidal category — in practice I say a category is “monoidal closed” too.

On the other hand, where you say “closed”, I say “cartesian closed”, using the categorical product as the monoidal structure. I choose the linguistically more general term to refer to the mathematically more general concept.

Comment by John Armstrong | September 10, 2007 |

My point is that you are being unnecessarily restrictive in confining yourself to situations where you have a monoidal structure which has an associated closed structure. Moreover, it is not historically correct: category theorists originally defined closed categories without tensors (i.e. only with a notion of internal

hom [-,-] axiomatized appropriately). In addition to the

original paper I mentioned in my post above, a very nice

paper is by M. LaPlaza (Trans. AMS, 1977, entitled

“Coherence in nonmonoidal closed categories”. It is not a question of language but rather a question

of what one takes as primitive. This is true in logic as well, where one has systems of logic based on implication, without there being an associated “conjunction” or “tensor”. Cartesian Closed, Monoidal Closed, etc. are all examples of the more general (and mathematical useful) notion of closed (but not-necessarily-monoidal”) category.

Comment by Philip Scott | September 20, 2007 |

I will grant you, though, that most mathematicians would

consider monoidal structure (products, tensors, etc)

in conjunction with closedness more natural and highly desirable (rather than having huge towers of exponentials, which rapidly become unwieldy). But on the other hand,

for logicians and computer scientists it is not so straight-forward: many technical theorems in lambda calculus and proof theory are inherently simpler if you don’t have product types (with surjective pairing) floating around.

(and, in the untyped lambda calculus, surjective

pairing is actually quite problematic).

Comment by Philip Scott | September 20, 2007 |

While there may be some examples, I honestly can’t think of them as more than toys. In what sense is something a “logic” if you can’t even say “and” in it?

Besides, I’m not writing a technical treatise here, and I am not Bourbakishly insisting on doing everything in the utmost generality. And I don’t see how it’s “all wrong” (that’s a very rude way to put it, you know), since my terms mean exactly what I say they mean. And I can point to many other mathematicians who use these terms in exactly the same way. I’m sorry we don’t measure up to your lofty standards, but you’re free to work your mathematics in your own way.

Comment by John Armstrong | September 27, 2007 |

Well a real-life example of a useful logic with only ‘if’ would be (intuitionistic) implicational linear logic, which can be used for assembling meanings for certain kinds of theories of natural language, as discussed at a rather elementary level in various papers on my web-page, and in a more sophisticated way in recent dissertations by Iddo Lev (http://www.geocities.com/iddolev/Papers.html#_pulc) and Ash Asudeh (http://http-server.carleton.ca/~asudeh/). There is a real issue as to whether ‘and’ is actually needed (Asudeh uses it, Lev doesn’t), and it certainly creates various technical nuisances.

An interesting blog with some coverage of logic & category theory is Jon Cohen’s http://thatlogicblog.blogspot.com/; it hasn’t been very active recently, but hopefully it will resume someday.

Comment by Avery Andrews | September 28, 2007 |

Attempt to fix links:

Iddo Lev

Ash Asudeh

Jonathan Cohen

Comment by Avery Andrews | September 28, 2007 |

Trying to restate the point here, there seem to be contexts where one would want there to exist an appropriately monoidal left adjoint to the exponential, but formalisms which explicitly use it for anything are messy (e.g. the -elimination rule in linear logic.

So, a question for Philip Scott, are there situations where there is something that acts enough like implication to deserve the name, but lacks the appropriate left adjoint?

Comment by MathOutsider | September 29, 2007 |

Attempting to answer the above, various logics with ‘if’ but not ‘and’ provide examples of CCs that aren’t monoidal, e.g.

the HCC system from Mints (1976) ‘Closed Categories and the Theory of Proofs’, but Laplaza (1977) ‘Embedding of Closed Categories Into Monoidal Closed Categories’ shows that any closed category can be embedded into a monoidal (bi-)closed one, which seems to me to mean that ‘and’ can be provided if you want it (uniquely, by virtue of adjunction).

So isn’t that like division w.r.t. the integers, one might leave fractions out of a particular formalized system, but aren’t they nevertheless essentially present?

Comment by MathOutsider | October 4, 2007 |

[...] category is also monoidal closed. There are various natural monoidal structures we could use, so we’ll start with the [...]

Pingback by Ordered Linear Spaces II « The Unapologetic Mathematician | May 15, 2009 |