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 |0|, is initial iff for every object in the category there exists a unique arrow from |0|. If |A| is an object in the category, we can write |\langle A\rangle : 0 \to A| for the unique arrow.
Representability isn’t as simple or intuitive as initiality, but it is still pretty simple.
A functor |F : \mathcal{C}^{op} \to \mathbf{Set}| is representable iff |F \cong \mathrm{Hom}(-,Y)| for some |Y|. Note that this is an isomorphism between functors, i.e. a natural isomorphism. We say |Y| represents the functor |F|. A functor |G : \mathcal{C} \to \mathbf{Set}| is co-representable iff |G \cong \mathrm{Hom}(X,-)| (co-)represents the functor |G|. Representable and co-representable aren’t actually different; if we set |\mathcal C = \mathcal D^{op}| then we could say |F| is co-representable as a functor from |\mathcal D| and it would mean the same thing.
Now we need to prove initiality and (co-)representability equivalent. One direction is easy, |0| co-represents the functor |\lambda C. \{\star\}|.1 It’s easy to show that this says exactly that |0| is initial.
I’ll hold off on the other direction and instead prove the circular implication: Representability |\Rightarrow| Initiality |\Rightarrow| Universal Arrow |\Rightarrow| Representability. Right now we’ve done the first step; we can recast initiality as representability. Next we’ll show that we can recast universal arrows as initiality and representability as a universal arrow and we’ll have shown them all equivalent.
Let |U : \mathcal C \to \mathcal D| be a functor. |\eta : A \to UX| is a universal arrow iff for all |f : A \to UY| there exists a unique arrow |\langle f\rangle : X \to Y| such that |f = U\langle f\rangle \circ \eta|. Dually, let |F : \mathcal C \to \mathcal D| be a functor, then |\varepsilon : FX \to A| is a co-universal arrow iff for all |g : FY \to A| there exists a unique arrow |\langle g\rangle : Y \to X| such that |g = \varepsilon \circ F\langle g\rangle|. Again, these are equivalent notions. A co-universal arrow is just a universal arrow in the opposite category.
Now to prove Initiality |\Rightarrow| Universal Arrow. Consider the (comma) category whose objects are pairs |(f, Y)| where |f : A \to UY| and whose arrows |k : (f, Y) \to (g, Z)| are arrows |k : Y \to Z| such that |g = Uk \circ f|. |\eta| is a universal arrow iff |(\eta, X)| is initial in this category. This is easy to check.
Finally, Universal Arrow |\Rightarrow| Representability. Let |G : \mathcal C \to \mathbf{Set}|. The claim is there exists a universal arrow |\eta : \{\star\} \to GX| iff |X| co-represents |G|. Doing the backwards direction first, if |X| co-represents |G| then there is an element of |GX| that corresponds to |\mathrm{id} : X \to X|. Have |\eta| pick out that element. Given another element |y : \{\star\} \to GY| we need to find a unique arrow |\langle y\rangle : X \to Y| such that |G\langle y\rangle(\eta) = y|. Naturality of the isomorphism making |X| co-represent |G| says: |f \circ \phi_A(a) = \phi_B(Gf(a))| where |\phi : G \cong \mathrm{Hom}(X,-)|, |f : A \to B|, and |a \in GA|. Applying |\phi_Y| to both sides of the earlier equation and using |\phi_X(\eta) = \mathrm{id}| we get: |\langle y\rangle = \phi_Y(y)| showing that |\langle y\rangle| exists and is unique and thus |\eta| is a universal arrow.
Next we need to show that |\eta : \{\star\} \to GX| being a universal arrow implies that |X| co-represents |G|. We immediately have a parameterized bijection namely |\langle -\rangle_Y : GY \cong \mathrm{Hom}(X,Y)|. All we need to do is show that it is natural in |Y| which is to say |f \circ \langle a\rangle_A = \langle Gf(a)\rangle_B| where |f : A \to B|. We have |Gf(a) = Gf(G\langle a\rangle(\eta)) = (Gf \circ G\langle a\rangle)(\eta) = G(f \circ \langle a\rangle)(\eta)|. Using |f = \langle Gf(\eta)\rangle_B| which is a consequence of |\eta| being universal, we get |\langle Gf(a)\rangle_B = f \circ \langle a\rangle_A| as desired.
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 |F|-algebras for some functor |F|. (Incidentally, the category of |F|-algebras is a subcategory of a comma category.)
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 |\mathrm{Hom}(FA,B) \cong \mathrm{Hom}(A,UB)|. In particular, the intimate connection between ends/indexed limits and sets of natural transformations significantly eases moving up and down functor categories.
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.
|\{\star\}| is just some singleton set.↩︎