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

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?
As promised, I'm finally going to get to the theory behind monads. As a quick review, the basic idea of the monad in Haskell is a hidden transition function - a monad is, basically, a state transition function.
So, we're still working towards showing the relationship between linear logic and category theory. As I've already hinted, linear logic has something to do with certain monoidal categories. So today, we'll get one step closer, by talking about just what kind of monoidal category.
One of the questions that a ton of people sent me when I said I was going to write about category theory was "Oh, good, can you please explain what the heck a *monad* is?"