Arguably (1-)category theory is the study of universal properties. There are three standard formulations of the notion of universal property which are all equivalent. Most introductions to category theory will cover all three and how they relate. By systematically preferring one formulation above the others, three styles of doing category theory arise with distinctive constructions and proof styles.
I noticed this trichotomy many years ago, but I haven’t heard anyone explicitly identify and compare these styles. Furthermore, in my opinion, one of these styles, the one I call Set-category theory, is significantly easier to use than the others, but seems poorly represented in introductions to category theory.
For myself, it wasn’t until I read Basic Concepts of Enriched Category Theory by G. M. Kelly and was introduced to indexed (co)limits (aka weighted (co)limits), that I began to recognize and appreciate Set-category theory. Indexed (co)limits are virtually absent from category theory introductions, and the closely related notion of (co)ends are also very weakly represented despite being far more useful than (conical) (co)limits. I don’t know why this is. Below I’ll be more focused on comparing the styles than illustrating the usefulness of indexed (co)limits. I may write an article about that in the future; in the mean time you can read “Basic Concepts of Enriched Category Theory” and just ignore the enriched aspect. Admittedly, it is definitely not an introduction to category theory.
What follows are three equivalent formulations of the notion of universal property including proofs of equivalence.
Initiality is by far the simplest formulation of universal properties to understand because it is a very special case, albeit a special case that can be finagled to cover the general case.
An object, typically denoted
Representability isn’t as simple or intuitive as initiality, but it is still pretty simple.
A functor
Now we need to prove initiality and (co-)representability equivalent. One direction is easy,
I’ll hold off on the other direction and instead prove the circular implication: Representability
Let
Now to prove Initiality
Finally, Universal Arrow
Next we need to show that
In the initiality style of doing category theory, the main exercise is defining an appropriate category. This is pretty difficult from both a creativity perspective and a notational perspective. Once an appropriate category is defined, though, the proofs are typically not too hard. Perhaps the main tool is the comma category as that allows the compact and flexible specification of many categories, though it can often take a touch of creativity to recognize a category as a comma category. Technically, the proof above implies that for any universal property there’s an appropriate comma category in which the universal object is the initial object.
This style is often seen in introductions to category theory. If you’ve ever read about categories of
(co)cones or wedges, then you’ve seen an example of this style with an ad-hoc definition of the relevant
categories. In practice, the categories needed to characterize a specific universal property are of little
interest on their own so the effort spent defining them isn’t repaid. The main exception is the category
of
The style of proof is to leverage the uniqueness of the mediating morphism to equate two seemingly different things. Lambek’s lemma is an excellent illustration of this proof style.
The core of this style of category theory is representability and its parameterized variant. Representability alone is already very powerful and ergonomic. Every limit or colimit in a category represents a limit of homsets. This means all the tools and intuitions of set theory are available. This is the basis for my naming of this style: we elucidate the structure of a category by relating it to the structure of the category of sets.
The main tools of this style are (co)ends, indexed (co)limits, and adjunctions in the form
By far the best part of this approach is the style of proof. By leveraging continuity properties, characterizations in terms of (parameterized) representability, some general isomorphisms, and occasionally some hand-crafted isomorphisms, nearly any categorical theorem can be proven in a dozen or less isomorphisms. The presentation looks and feels very much like solving an algebraic equation. The proofs are easy to read and easy to write.
The main drawback of this style is that most of the properties above weaken and some disappear when working in enriched or higher categories.
Arguably, this style should be based on universal arrows. While it technically is, in practice, it’s rare that one talks about universal arrows and instead the parameterized version, namely adjunctions in their unit/counit formulation are the main tool. After adjunctions would be Kan extensions. All of these are concepts that live naturally at the level of 2-categories which makes them much easier to generalize.
The main style of proof is diagram chasing, i.e. proving typically several equalities. On the one hand, proving an equation is straight-forward equational reasoning; on the other hand, there tend to be several equations that need to be proven at a time, they tend to be fine-grained and thus detailed and tedious, and often general results don’t obviously apply. The solution to most of these problems is to use string diagrams instead. Many of the bureaucratic details completely disappear and the proofs become crystal clear. A wonderful example of this style of proof is proving that an adjunction gives rise to a monad. With normal diagram chasing it’s mildly tedious. With string diagrams it proves itself.
One issue that comes up in this style is the elegant definitions tend to be wholesale. For example, there’s a nice adjunction that characterizes all limits of any given shape. Unfortunately, the adjunction only exists if all the limits of that shape exists. If they don’t all exist, then you need to use some other method to talk about the limits that do exist. Technically, universal arrows could handle this, but usually representability is used instead.
Ultimately, one should become familiar with all these approaches. There are definitely problems that fit nicer in some than others. However, when it comes to universal properties the Set-category theory wins hands down. Cat-category theory tends to be more useful when working with structures that aren’t characterized by a universal property such as monoidal structure. Initiality has its niche with initial algebras. I don’t have any ideas on where it might also be a profitable perspective. In fact, I’m not completely sure it’s a good thing that we think about initial algebras as initial algebras. There are interesting interactions between initial algebras and adjunctions for example and it’s not clear to me that they wouldn’t be more accessible with a different presentation of initial algebras.