Previously in this series we’ve seen the definition of a category and a bunch of examples, basic properties of morphisms, and a first look at how to represent categories as types in ML. In this post we’ll expand these ideas and introduce the notion of a universal property. We’ll see examples from mathematics and write some programs which simultaneously prove certain objects have universal properties and construct the morphisms involved.

A Grand Simple Thing

One might go so far as to call universal properties the most important concept in category theory. This should initially strike the reader as odd, because at first glance universal properties are so succinctly described that they don’t seem to be very interesting. In fact, there are only two universal properties and they are that of being initial and final.

Definition: An object in a category is called initial if for every object there is a unique morphism . An object is called final if for every object there is a unique morphism . If an object satisfies either of these properties, it is called universal. If an object satisfies both, it is called a zero object.

In both cases, the existence of a unique morphism is the same as saying the relevant Hom set is a singleton (i.e., for initial objects , the Hom set consists of a single element). There is one and only one morphism between the two objects. In the particular case of when is initial (or final), the definition of a category says there must be at least one morphism, the identity, and the universal property says there is no other.

There’s only one way such a simple definition could find fruitful applications, and that is by cleverly picking categories. Before we get to constructing interesting categories with useful universal objects, let’s recognize some universal objects in categories we already know.

In the single element set is final, but not initial; there is only one set-function to a single-element set. It is important to note that the single-element set is far from unique. There are infinitely many (uncountably many!) singleton sets, but as we have already seen all one-element sets are isomorphic in (they all have the same cardinality). On the other hand, the empty set is initial, since the “empty function” is the only set-mapping from the empty set to any set. Here the initial object truly is unique, and not just up to isomorphism.

It turns out universal objects are always unique up to isomorphism, when they exist. Here is the official statement.

Proposition: If are both initial in , then are isomorphic. If are both final, then .

Proof. Recall that a mophism is an isomorphism if it has a two sided inverse, a so that and are the identities. Now if are two initial objects there are unique morphisms and . Moreover, these compose to be morphisms . But since is initial, the only morphism is the identity. The situation for is analogous, and so these morphisms are actually inverses of each other, and are isomorphic. The proof for final objects is identical.

Let’s continue with examples. In the category of groups, the trivial group is both initial and final, because group homomorphisms must preserve the identity element. Hence the trivial group is a zero object. Again, “the” trivial group is not unique, but unique up to isomorphism.

In the category of types with computable (halting) functions as morphisms, the null type is final. To be honest, this depends on how we determine whether two computable functions are “equal.” In this case, we only care about the set of inputs and outputs, and for the null type all computable functions have the same output: null.

Partial order categories are examples of categories which need not have universal objects. If the partial order is constructed from subsets of a set , then the initial object is the empty set (by virtue of being a subset of every set), and as a subset of itself is obviously final. But there are other partial orders, such as inequality of integers, which have no “smallest” or “largest” objects. Partial order categories which have particularly nice properties (such as initial and final objects, but not quite exactly) are closely related to the concept of a domain in denotational semantics, and the language of universal properties is relevant to that discussion as well.

The place where universal properties really shine is in defining new constructions. For instance, the direct product of sets is defined by the fact that it satisfies a universal property. Such constructions abound in category theory, and they work via the ‘diagram categories’ we defined in our introductory post. Let’s investigate them now.

Quotients

Let’s recall the classical definition from set theory of a quotient. We described special versions of quotients in the categories of groups and topological spaces, and we’ll see them all unified via the universal property of a quotient in a moment.

Definition: An equivalence relation on a set is a subset of the set product which is reflexive, symmetric, and transitive. The quotient set is the set of equivalence classes on . The canonical projection is the map sending to its equivalence class under .

The quotient set can also be described in terms of a special property: it is the “largest” set which agrees with the equivalence relation . On one hand, it is the case that whenever in then . Moreover, for any set and any map which equates equivalent things ( for all ), then there is a unique map such that . This word salad is best translated into a diagram.

Here we use a dashed line to assert the existence of a morphism (once we’ve proven such a morphism exists, we use a solid line instead), and the symbol signifies existence () and uniqueness (!).

We can prove this explicitly in the category . Indeed, if is any map such that for all equivalent , then we can define as follows: for any whose equivalence class is denoted by in , and define . This map is well defined because if , then . It is unique because if for some other , then ; this is the only possible definition.

Now the “official” way to state this universal property is as follows:

The quotient set is universal with respect to the property of mapping to a set so that equivalent elements have the same image.

But as we said earlier, there are only two kinds of universal properties: initial and final. Now this looks suspiciously like an initial object ( is going from , after all), but what exactly is the category we’re considering? The trick to dissecting this sentence is to notice that this is not a statement about just , but of the morphism .

That is, we’re considering a diagram category. In more detail: fix an object in and an equivalence relation on . We define a category as follows. The objects in the category are morphisms such that in implies in . The morphisms in the category are commutative diagrams

Here need to be such that they send equivalent things to equal things (or they wouldn’t be objects in the category!), and by the commutativity of the diagram . Indeed, the statement about quotients is that is an initial object in this category. In fact, we have already proved it! But note the abuse of language in our offset statement above: it’s not really that is the universal object, but . Moreover, the statement itself doesn’t tell us what category to inspect, nor whether we care about initial or final objects in that category. Unfortunately this abuse of language is widespread in the mathematical world, and for arguably good reason. Once one gets acquainted with these kinds of constructions, reading between the limes becomes much easier and it would be a waste of time to spell it out. After all, once we understand there is no “obvious” choice for a map except for the projection . This is how got its name, the canonical projection.

Two last bits of terminology: if is any category whose objects are sets (and hence, where equivalence relations make sense), we say that has quotients if for every object there is a morphism satisfying the universal property of a quotient. Another way to state the universal property is to say that all maps respecting the equivalence structure factor through the quotient, in the sense that we get a diagram like the one above.

What is the benefit of viewing by its universal property? For one, the set is unique up to isomorphism. That is, if any other pair satisfies the same property, we automatically get an isomorphism . For instance, if is defined via a function (that is, if ), then the pair satisfies the universal property of a quotient. This means that we can “decompose” any function into three pieces:

The first map is the canonical projection, the second is the isomorphism given by the universal property of the quotient, and the last is the inclusion map into . In a sense, all three of these maps are “canonical.” This isn’t so magical for set-maps, but the same statement (and essentially the same proof) holds for groups and topological spaces, and are revered as theorems. For groups, this is called The First Isomorphism Theorem, but it’s essentially the claim that the category of groups has quotients.

This is getting a bit abstract, so let’s see how the idea manifests itself as a program. In fact, it’s embarrassingly simple. Using our “simpler” ML definition of a category from last time, the constructive proof that quotient sets satisfy the universal property is simply a concrete version of the definition of we gave above. In code,

fun inducedMapFromQuotient(setMap(x, pi, q), setMap(x, g, y)) =
   setMap(q, (fn a => g(representative(a))), y)

That is, once we have and defined for our given equivalence relation, this function accepts as input any morphism and produces the uniquely defined in the diagram above. Here the “representative” function just returns an arbitrary element of the given set, which we added to the abstract datatype for sets. If the set is empty, then all functions involved will raise an “empty” exception upon being called, which is perfectly fine. We leave the functions which explicitly construct the quotient set given as an exercise to the reader.

Products and Coproducts

Just as the concept of a quotient set or quotient group can be generalized to a universal property, so can the notion of a product. Again we take our intuition from . There the product of two sets is the set of ordered pairs

But as with quotients, there’s much more going on and the key is in the morphisms. Specifically, there are two obvious choices for morphisms and . These are the two projections onto the components, namely and . These projections are also called “canonical projections,” and they satisfy their own universal property.

The product of sets is universal with respect to the property of having two morphisms to its factors.

Indeed, this idea is so general that it can be formulated in any category, not just categories whose objects are sets. Let be two fixed objects in a category . Should it exist, the product is defined to be a final object in the following diagram category. This category has as objects pairs of morphisms

and as morphisms it has commutative diagrams

In words, to say products are final is to say that for any object in this category, there is a unique map that factors through the product, so that  and . In a diagram, it is to claim the following commutes:

If the product exists for any pair of objects, we declare that the category has products.

Indeed, many familiar product constructions exist in pure mathematics: sets, groups, topological spaces, vector spaces, and rings all have products. In fact, so does the category of ML types. Given two types ‘a and ‘b, we can form the (aptly named) product type ‘a * ‘b. The canonical projections exist because ML supports parametric polymorphism. They are

fun leftProjection(x,y) = x
fun rightProjection(x,y) = y

And to construct the unique morphism to the product,

fun inducedMapToProduct(f,g) = fn a => (f(a), g(a))

We leave the uniqueness proof to the reader as a brief exercise.

There is a similar notion called a coproduct, denoted , in which everything is reversed: the arrows in the diagram category go to and the object is initial in the diagram category. Explicitly, for a fixed the objects in the diagram category are again pairs of morphisms, but this time with arrows going to the central object

The morphisms are again commutative diagrams, but with the connecting morphism going away from the central object

And a coproduct is defined to be an initial object in this category. That is, a pair of morphisms such that there is a unique connecting morphism in the following diagram.

Coproducts are far less intuitive than products in their concrete realizations, but the universal property is no more complicated.  For the category of sets, the coproduct is a disjoint union (in which shared elements of two sets are forcibly considered different), and the canonical morphisms are “inclusion” maps (hence the switch from to in the diagram above). Specifically, if we define the coproduct

as the set of “tagged” elements (the right entry in a tuple signifies which piece of the coproduct the left entry came from), then the inclusion maps and are the canonical morphisms.

There are similar notions of disjoint unions for topological spaces and graphs, which are their categories’ respective coproducts. However, in most categories the coproducts are dramatically different from “unions.” In group theory, it is a somewhat complicated object known as the free product. We mentioned free products in our hasty discussion of the fundamental group, but understanding why and where free groups naturally occur is quite technical. Similarly, coproducts of vector spaces (or -modules) are more like a product, with the stipulation that at most finitely many of the entries of a tuple are nonzero (e.g., formal linear combinations of things from the pieces). Even without understanding these examples, the reader should begin to believe that relatively simple universal properties can yield very useful objects with potentially difficult constructions in specific categories. The ubiquity of the concepts across drastically different fields of mathematics is part of why universal properties are called “universal.”

Luckily, the category of ML types has a nice coproduct which feels like a union, but it is not supported as a “native” language feature like products types are. Specifically, given two types ‘a, ‘b we can define the “coproduct type”

datatype ('a, 'b)Coproduct = left of 'a | right of 'b

Let’s prove this is actually a coproduct: fix two types ‘a and ‘b, and let be the functions

fun leftInclusion(x) = left(x)
fun rightInclusion(y) = right(y)

Then given any other pair of functions which accept as input types ‘a and ‘b, respectively, there is a unique function operating on the coproduct type. We construct it as follows.

fun inducedCoproductMap(f,g) =
   let
      theMap(left(a)) = f(a)
      theMap(right(b)) = g(b)
   in
      theMap
   end

The uniqueness of this construction is self-evident. This author finds it fascinating that these definitions are so deep and profound (indeed, category theory is heralded as the queen of abstraction), but their realizations are trivially obvious to the working programmer. Perhaps this is a statement about how well-behaved the category of ML types is.

Continuing On

So far we have seen three relatively simple examples of universal properties, and explored how they are realized in some categories. We should note before closing two things. The first is that not every category has objects with these universal properties. Unfortunately poset categories don’t serve as a good counterexample for this (they have both products and coproducts; what are they?), but it may be the case that in some categories only some pairs of objects have products or coproducts, while others do not.

Second, there are many more universal properties that we haven’t covered here. For instance, the notion of a limit is a universal property, as is the notion of a “free” object. There are kernels, pull-backs, equalizers, and many other ad-hoc universal properties without names. And for every universal property there is a corresponding “dual” property that results from reversing the arrows in every diagram, as we did with coproducts. We will visit the relevant ones as they come up in our explorations.

In the next few posts we’ll encounter functors and the concept of functoriality, and start asking some poignant questions about familiar programmatic constructions.

Until then!