Using Natural Transformations: Recreating Closed Cartesian Categories

Today's contribution on category theory is going to be short and sweet. It's an example of why we really care about [natural transformations][nt]. Remember the trouble we went through working up to define [cartesian categories and cartesian closed categories][ccc]?

As a reminder: a [functor][functor] is a structure preserving mapping between categories. (Functors are the morphisms of the category of small categories); natural transformations are structure-preserving mappings between functors (and are morphisms in the category of functors).

Since we know that the natural transformation can be viewed as a kind of arrow, then we can take the definitions of iso-, epi-, and mono-morphisms, and apply them to natural transformations, resulting in *natural isomorphisms*, *natural monomorphisms*, and *natural epimorphisms*.

Expressed this way, a cartesian category is a category C where:

1. C contains a terminal object t; and
2. (∀ a,b ∈ Obj(C)), C contains a product object a×b; and
a *natural isomorphism* Δ, which maps each Functor over (C×C): ((x → a) → b) to (x → (a×b))

What this really says is: if we look at categorical products, then for a cartesian category, there's a way of understanding the product as a
mapping within the category as a pairing structure over arrows.

structure-preserving transformation from arrows between the pairs of values (a,b) and the products (a×b).

The closed cartesian category is just the same exact trick using the exponential: A CCC is a category C where:

1. C is a cartesian category, and
2. (∀ a,b ∈ Obj(C)), C contains an object ba, and a natural isomorphism Λ, where (∀ y ∈ Obj(C)) Λ : (y×a → b) → (y → ab).

Look at these definitions; then go back and look at the old definitions that we used without the new constructions of the natural transformation. That will let you see what all the work to define natural transformations buys us. Category theory is all about structure; with categories, functors, and natural transformations, we have the ability to talk about extremely sophisticated structures and transformations using a really simple, clean abstraction.

[functor]: http://scienceblogs.com/goodmath/2006/06/more_category_theory_getting_i…
[nt]: http://scienceblogs.com/goodmath/2006/06/category_theory_natural_transf…
[ccc]: http://scienceblogs.com/goodmath/2006/06/categories_products_exponentia…

More like this

So, at last, we can get to Yoneda's lemma, as I [promised earlier][yoneda-promise]. What Yoneda's lemma does is show us how for many categories (in fact, most of the ones that are interesting) we can take the category C, and understand it using a structure formed from the functors from C to the…
Let's talk a bit about functors. Functors are fun! What's a functor? I already gave the short definition: a structure-preserving mapping between categories. Let's be a bit more formal. What does the structure-preserving property mean? A functor F from category C to category D is a mapping from C…
Suppose we've got a topological space. So far, in our discussion of topology, we've tended to focus either very narrowly on local properties of **T** (as in manifolds, where locally, the space appears euclidean), or on global properties of **T**. We haven't done much to *connect* those two views.…
Today we'll finally get to building the categories that provide the model for the multiplicative linear logic. Before we jump into that, I want to explain why it is that we separate out the multiplicative part. Remember from the simply typed lambda calculus, that [we showed that the type system was…