# category theory

### Meta out the wazoo: Monads and Monoids

Since I mentioned the idea of monoids as a formal models of computations, John Armstrong made the natural leap ahead, to the connection between monoids and monads - which are a common feature in programming language semantics, and a prominent language feature in href="http://scienceblogs.com/goodmath/goodmath/programming/haskell/">Haskell, one of my favorite programming languages. Monads are a category theoretic construction. If you take a monoid, and use some of the constructions we've seen in the last few posts, we can move build a meta-monoid; that is, a monoid that's built from…

### Full Circle: the Categorical Monoid

By now, we've seen the simple algebraic monoid, which is essentially an abstract construction of a category. We've also seen the more complicated, but interesting monoidal category - which is, sort of, a meta-category - a category built using categories. The monoidal category is a fairly complicated object - but it's useful. What does a algebraic monoid look like in category theory? The categorical monoid is a complex object - a monoid built from monoids. If we render the algebraic monoid in terms of a basic category, what do we get? A monoid is, basically, a category with one object. That'…

### This is getting fun! On to Monoidal Categories.

In the last post on groups and related stuff, I talked about the algebraic construction of monoids. A monoid is, basically, the algebraic construction of a category - it's based on the same ideas, and has the same properties; just the presentation of it is different. But you can also see a monoid in categorical terms. It's what we computer scientists would call a bootstrapped definition: we're relying on the fact that we have all of the constructs of category theory, and then using category theory to rebuild its own basic concepts. The basic idea of the construction is to start pretty much…

### Clarifying Groupoids and Groups

This post started out as a response to a question in the comments of my last post on groupoids. Answering those questions, and thinking more about the answers while sitting on the train during my commute, I realized that I left out some important things that were clear to me from thinking about this stuff as I did the research to write the article, but which I never made clear in my explanations. I'll try to remedy that with this post. So - in the last post I explained a bit about the categorical viewpoint on why we should care about groupoids. Every groupoid contains groups. The groups…

### More Groupoids and Groups

In my introduction to groupoids, I mentioned that if you have a groupoid, you can find groups within it. Given a groupoid in categorical form, if you take any object in the groupoid, and collect up the paths through morphisms from that object back to itself, then that collection will form a group. Today, I'm going to explore a bit more of the relationship between groupoids and groups. Before I get into it, I'd like to do two things. First, a mea culpa: this stuff is out on the edge of what I really understand. My category-theory-foo isn't great, and I'm definitely on thin ice here. I think…

### Capturing More Symmetry using Categories: Groupoids

Today's entry is short, but sweet. I wanted to write something longer, but I'm very busy at work, so this is what you get. I think it's worth posting despite its brevity. When we look at groups, one of the problems that we can notice is that there are things that seem to be symmetric, but which don't work as groups. What that means is that despite the claim that group theory defines symmetry, that's not really entirely true. My favorite example of this is the fifteen puzzle. The fifteen puzzle is a four-by-four grid filled with 15 tiles, numbered from 1 to 15, and one empty space. You can…

### Before Groups from Categories: a Category Refresher

So far, I've spent some time talking about groups and what they mean. I've also given a brief look at the structures that can be built by adding properties and operations to groups - specifically rings and fields. Now, I'm going to start over, looking at things using category theory. Today, I'll start with a very quick refresher on category theory, and then I'll give you a category theoretic presentation of group theory. I did a whole series of articles about category theory right after I moved GM/BM to ScienceBlogs; if you want to read more about category theory than this brief…

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. The theory of monads comes from category theory. I'm going to assume you know a little bit about category theory - if you have trouble with it, go take a look at my introductory posts here. Fundamentally, in category theory a monad is a category with a particular kind of structure. It's a category with one object. That category has a collection of arrows which (obviously) are from…

### Big to Small, Small to Big: Topological Properties through Sheaves (part 1)

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. How do we get from local properties to global properties? One of the tools for doing that is a sheaf (plural "sheaves"). A sheaf is a very general kind of structure that provides ways of mapping or relating local information about a topological space to global information about that space. There are…

### Topological Products Redux: Categories to the rescue!

This is going to be a short but sweet post on topology. Remember way back when I started writing about category theory? I said that the reason for doing that was because it's such a useful tool for talking about other things. Well, today, I'm going to show you a great example of that. Last friday, I went through a fairly traditional approach to describing the topological product. The traditional approach not *very* difficult, but it's not particularly easy to follow either. The construction isn't really that difficult, but it's not easy to work out just what it all really means. There is…

### From Lambda Calculus to Cartesian Closed Categories

This is one of the last posts in my series on category theory; and it's a two parter. What I'm going to do in these two posts is show the correspondence between lambda calculus and the [cartesian closed categories][ccc]. If you're not familiar with lambda calculus, you can take a look at my series of articles on it [here][lambda]. You might also want to follow the CCC link above, to remind yourself about the CCCs. (The short refresher is: a CCC is a category that has an exponent and a product, and is closed over both. The product is an abstract version of cartesian set product; the exponent…

### Categorical Numbers

Sorry for the delay in the category theory articles. I've been busy with work, and haven't had time to do the research to be able to properly write up the last major topic that I plan to cover in cat theory. While doing my research on closed cartesian categories and lambda calculus, I came across this little tidbit that I hadn't seen before, and I thought it would be worth taking a brief diversion to look at. Category theory is sufficiently powerful that you can build all of mathematics from it. This is something that we've known for a long time. But it's not really the easiest thing to…

### The Categorical Model of Linear Logic

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 precisely a subset of intuitionistic logic][lambda-type], and that programs in the lambda calculus corresponded to proofs in the type system. In particular, it was propositional intuitionistic logic using only the "→" operation. Similarly, if you build up a more interesting typed lambda calculus…

### Zeros in Category Theory

Things are a bit busy at work on my real job lately, and I don't have time to put together as detailed a post for today as I'd like. Frankly, looking at it, my cat theory post yesterday was half-baked at best; I should have held off until I could polish it a bit and make it more comprehensible. So I'm going to avoid that error today. Since we've had an interesting discussion focusing on the number zero, I thought it would be fun to show what zero means in category theory. There are two zeros it category theory: the zero object, and the zero arrow. Zero Objects -------------- The zero object…

### The Category Structure for Linear Logic

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. As I keep complaining, the problem with category theory is that anytime you want to do something interesting, you have to wade through a bunch of definitions to set up your structures. I'll do my best to keep it short and sweet; as short as it is, it'll probably take a bit of time to sink in. First, we need a…

### Towards a Model for Linear Logic: Monoidal Categories

Time to come back to category theory from out side-trip. Category theory provides a good framework for defining linear logic - and for building a Curry-Howard style type system for describing computations with *state* that evolves over time. Linear logic provides a way of defining a valid *model* for part of linear logic (the multiplicative operators) that aren't tractable using other modeling techniques. I'm going to show you the relationship between models for linear logic and category theory. It's going to take a couple of days to go through the whole shebang, but even the parts that we…

### Linear Logic

[Monday][yesterday], I said that I needed to introduce the sequent calculus, because it would be useful for describing things like linear logic. Today we're going to take a quick look at linear logic - in particular, at *propositional* linear logic; you can expand to predicate linear logic in a way very similar to the way we went from propositional logic to first order predicate logic. So first: what the heck *is* linear logic? The answer is, basically, logic where statements are treated as *resources*. So using a statement in an inference step in linear logic *consumes* the resource. This is…

### A Brief Diversion: Sequent Calculus

*(This post has been modified to correct some errors and add some clarifications in response to comments from alert readers. Thanks for the corrections!)* Today, we're going to take a brief diversion from category theory to play with some logic. There are some really neat connections between variant logics and category theory. I'm planning on showing a bit about the connections between category theory and one of those, called *linear logic* . But the easiest way to present things like linear logic is using a mechanism based on sequent calculus. Sequent calculus is a deduction system for…