Universal properties are a generalization of the notion of a Galois connection between two orderings. Or perhaps I should say: universal properties arise from adjunctions, and it is adjunctions that are a generalization of Galois connections. Adjunctions capture in an abstract categorical setting the idea of “optimal solutions to a problem”; and this idea is itself very general, capturing many of the structures underlying common patterns in programming (not to mention the rest of mathematics). Solutions to equations, products, limits of sequences of approximations, and minimality and maximality are just some of the instances of this powerful abstraction that we will make use of. In the preface to Categories for the Working Mathematician, Mac Lane wrote that “adjoint functors arise everywhere”.
Two functors and form an adjunction, written , if there is an isomorphism between the sets of arrows in and in . We say that is the left adjoint and the right adjoint. The essence of the isomorphism is captured by two natural transformations in and in , called the unit and counit of the adjunction; is the image in of in , and conversely, is the image in of in . The unit and counit satisfy the laws
From them one can construct the witnesses to the isomorphism for arbitrary arrows: for each arrow in , there is a unique arrow in such that , given by ; and conversely, for each arrow in , there is a unique arrow in such that , given by ; and moreover, these two constructions are each other’s inverses.
Adjunctions from Galois connections
A preorder forms a category: the objects of the category are the elements of the set~, and between any two elements , there is a unique arrow if , and no arrow otherwise. That adjunctions are a generalization of Galois connections follows straightforwardly from the fact that there is at most one arrow between any two objects in a preorder category. Then monotonic functions and between preorders and form a Galois connection precisely if the sets of arrows and are isomorphic—that is, if both and hold, or neither do, or in other words,
Adjoints of the diagonal functor
A very useful example of adjunctions arises in the definition of products—in the category of sets and total functions, for given types , there is an isomorphism between the set of pair-generating functions, of type , and their two projections, pairs of functions of types and . (Indeed, given functions and , one can construct the pair-generating function ; and conversely, given a pair-generating function , one can construct its two projections and ; and moreover, these two constructions are inverses.)
The “isomorphism between sets of arrows” can be elegantly expressed as an adjunction; since it concerns pairs of arrows, one side of the adjunction involves the product category . The right adjoint is the product functor , mapping an object in —that is, a pair of sets—to their cartesian product as an object in , and an arrow in —that is, a parallel pair of functions—to a function in acting pointwise on pairs. In the other direction, the left adjoint is the diagonal functor , mapping an object in to the object in , and a function to the pair of functions as an arrow in . The adjunction amounts to the isomorphism
The unit and counit of the adjunction are and . In more familiar terms, the unit is a natural transformation in , so a polymorphic function; in fact, it’s the function of type that we might call . However, the counit is a natural transformation in , so not simply a (polymorphic) function; but arrows in are pairs of functions, so we might write this .
Then the “fork” operation is in fact one of the two witnesses to the isomorphism between the sets of arrows: given an arrow in , that is, a pair of functions of types , then is an arrow in , that is, a function of type , given by the construction above:
or, with more points,
The laws that the unit and counit satisfy are
or, in more familiar terms,
The universal property of follows from the isomorphism between sets of arrows:
The universal property of underlies all the useful laws of that operator.
Of course, the situation nicely dualizes too. Coproducts in arise from the isomorphism between the set of arrows and the pairs of arrows in and . Again, “pairs of arrows” suggest the product category; but this time, the diagonal functor is the right adjoint, with the coproduct functor (which takes a pair of sets to their disjoint union) as the left adjoint. That is, the adjunction is , and the isomorphism is
The unit is a natural transformation in , that is, a pair of functions and . The counit is a natural transformation in , which we might call . The “join” of two functions with a common range is a witness to one half of the isomorphism—given an arrow in , then is an arrow in , defined by
The two laws that the unit and counit satisfy are:
or, perhaps more perspicuously,
Another familiar example from functional programming is the notion of currying, which arises when one can construct the function space (the type of functions from to , for each type and ), such that there is an isomorphism between the sets of arrows and . Here, the adjunction is —in this case, both functors are endofunctors on . The unit and counit are natural transformations and . We might call these and , since the first is a curried pair-forming operator, and the second applies a function to an argument:
The laws they satisfy are as follows:
or, in points,
The isomorphism itself is witnessed by the two inverse functions
where and .