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”.

## Adjoint functors

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

or equivalently,

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 .

While you haven’t yet mentioned (co)continuity of adjoints, which is one of the most valuable things about knowing that something is an adjoint, it’s nice to know that almost all the “high school algebra” rules that the naming and notation suggests follow immediately from (co)continuity of the adjoints defining a cartesian closed category, or indeed any symmetric monoidally closed category. (One of the ones that doesn’t is Ax1 ~ A, which is natural as the equivalent to that is an axiom of a monoidal category.)

However, to do this to the fullest extent requires recognizing another adjunction, of some importance, that exists in any symmetric monoidally closed category, and one that is rarely mentioned in contexts like this for reasons I don’t understand. Namely, (->B)^op -| (->B). Admittedly, in the CCC case, this doesn’t introduce any new constructs, it’s just a consequence. In the monoidally closed category case, though, asserting this adjunction is the same as asserting a symmetry via uncurry (flip (curry id)), though this is a bit roundabout. Of course, even as a consequence this is useful since it immediately gives things like (0->B) ~ 1 and ((A+B)->C) ~ (A->C)x(B->C).

I guess my unfamiliarity with (co-)continuity of adjoints is just a deeper manifestation of my similar unfamiliarity with the corresponding property of partial orders – that lower (upper) adjoints preserve joins (meets). I’m not aware of ever having had occasion to digest that…

Alan Schmitt has pointed out that I was a bit glib in my definition of adjunction. It’s not enough for there just to be an isomorphism phi between the hom-sets F(B)->A and A->G(B); it must be natural in A and B:

You need naturality to prove the two identity laws

Pingback: The Abstract Interpretation Monad | Eran's blag