# Practical Foundations of Mathematics

### Paul Taylor

Now we shall transform universal maps from their logically quantified statement into a purely algebraic form. This involves making a Choice (Exercise  3.26) of universal and co-universal maps, which provide the components of two natural transformations. Although they are unique up to unique isomorphism, these play a crucial role , and are just as much part of the definition as are the functors U and F. In particular we shall show that the laws which they obey express the b- and h-rules in type theory (Sections 2.3 and 2.7), and (as in Definition 4.7.2(c)) the naturality condition handles substitution or continuation.

In this section we drop the Convention 4.1.2 for brackets (which arose from Currying, Convention  2.3.2): F UA means F(UA), etc .

DEFINITION 7.2.1 An adjunction F\dashv U consists of

(a)
the right or upper adjoint functor U:A ® S,

(b)
the left or lower adjoint functor F:S ® A,

(c)
the unit natural transformation, h:\idS ® U·F, sometimes called the front adjunction, and

(d)
the co-unit natural transformation, e:F· U® \idA, also called the back adjunction,

satisfying the following triangular laws:

omitted diagram environment

cf Lemma 3.6.2 for posets. The letters L and R will be used to identify the triangles in the same way as N and Z for naturality in Definition  4.8.1.

THEOREM 7.2.2 The following are equivalent:

(a)

(b)
A natural isomorphism l:A(F(-),( = )) º S((-),U( = )), called the adjoint transposition ( cf Definition 3.6.1)
 omitted prooftree environment
is given between functors SopxA\twoheadrightarrow Set. (It is actually enough for l to be natural in one argument for each fixed object as the other.)

(c)
There is an assignment hX:X® U\typeAX of universal maps from each object X Î obS to the functor U.

(d)
There is an assignment eA:F\typeXA® A of co- universal maps from the functor F to each  A Î obA .

The components are derived from one another by

 omitted array environment
We shall break with our usual custom by deferring the proof to page  7.2.9.

REMARK 7.2.3 Naturality of l means that the following square in Set commutes, which, for p:F X® B, says that l(Fu;p;z) = u;l(p);Uz.

omitted diagram environment

Hence if the square on the left below commutes in A then so does that on the right in S (and conversely since l is bijective).

omitted diagram environment

Put z = id and compare these diagrams with Definition  4.7.2(c).

Applications   Recall from Sections 2.3 and 2.7 that the introduction, elimination, equality, b- and h-rules for the product, sum, function-type and List constructions are summed up by adjoint correspondences.

REMARK 7.2.4 Consider the common situation in which a universal property is used to define a new construction in terms of an old functor. Indeed the definition of universal maps, unlike that of adjunctions, was phrased in just this way.

(a)
The unit h provides the operations for the introduction rules, if these are direct (n0, n1, 0, +, empty list and append), and the co-unit e gives the direct operations for elimination (p0, p1, ev).

(b)
The triangle law on the old side is the b-rule.

(c)
The triangle law on the new side is extensionality or the h-rule . (It is a pity that the letter h has established meanings for two different parts of the anatomy of an adjunction.)

(d)
The adjoint transposition l is the meta-operation or indirect rule (l-abstraction, pairing, case analysis and recursion).

(e)
The naturality condition on the new side of the adjunction defines the effect of the new construction on morphisms.

(f)
Product and exponential are right adjoints, and naturality on the old side (the left) states the substitution-invariance of -,- and l.

(g)
For sum and List, which are left adjoints, old (right) naturality gives the continuation rules; in these cases substitution -invariance must be expressed by an extra condition.

EXAMPLE 7.2.5 For products, F:S® SxS is the diagonal functor and U = x. Then l is -,-, the co-unit e is the family of projections (pi) and the unit h is the diagonal map D:X® XxX. The product functor is defined on maps,

 omitted prooftree environment
by naturality on the right (the new side). The triangle laws are

 D;pi = id     and    D;(p0x p1) = id
or, type-theoretically, p0x,x = x, p1x,x = x and p0(z),p1(z) = z. We must use naturality of e to put the b-rules in the form p0x,y = x.

omitted diagram environment

Notice that y:1® Y is a global element: if it is only partially defined then commutativity of the square on the right becomes an inequality, so strict naturality fails in p-categories (Exercise  5.15).

EXAMPLE 7.2.6 For colimits, l-1 is case analysis [  ,  ], the unit h is the family of inclusions (ni) and the co-unit e is the codiagonal.

omitted diagram environment

The naturality condition on the left (the new side) defines + on maps. On the right (old) it states invariance under continuation z (Remark 2.3.13). This says that the (+E)- box is open-ended, cf Remark 1.6.5.

EXAMPLE 7.2.7 For function-types, F = (-)xY and U = ( = )Y. The adjoint transposition (l) is l-abstraction and the co-unit e is evaluation. Naturality on the left (the old side) states substitution-invariance of l (Definition  4.7.2(c)), and on the right (new) is postcomposition. The naturality of e is (-)X on morphisms; and that of h:x® ly.x,y is substitution under l.

The left triangle law is the essence of the b-rule, but in the special case p = x,y, (ly¢.x,y¢)y = x,y. To see it at work we must pre- and postcompose with the argument and the function, and use naturality, cf Remark 2.3.9.

omitted diagram environment

The right triangle law is the h-rule in a more direct way.

omitted diagram environment

EXAMPLE 7.2.8 List:Set® Mon is left adjoint to the forgetful functor. The unit is the singleton list, and the co-unit List(A)® A multiplies out a list of elements of the monoid A. The adjoint transposition l-1 is (roughly) what we called fold in Proposition 2.7.5 and [[-]] in Section 4.6 and elsewhere. Naturality on the left (the new side) for u:X® Y is the action mapu of the functor (Example 2.7.6(d)). On the right it is the action of a monoid homomorphism z (Remark  2.7.12).

Example 7.4.6 shows how eA:List(A)® A captures the structure of the algebra A.

REMARK 7.2.9 This account is connected with the binary rules for List ( append and fold) in Definition  2.7.4ff, whereas recursion in Section  6.1 was based on the unary form ( cons and listrec). The unary and binary theories employ universal properties in different ways, which are related to the different roles of the alphabet X.

(a)
The adjunction Mon\rightleftarrows Set describes all lists whatever, and we make use of the free monoid on any set of generators.

(b)
Definition 6.1.1 built X into the functor T, so we only use the initial T-algebra for recursion.

Proof of the equivalence   It is surprising how little structure need exist in advance: we need naturality of l on one side, for which we must know what the morphisms are. The rest of the structure is derivable: the naturality and triangle laws are the essential part.

PROOF OF THEOREM 7.2.2: We must show that the eight expressions are functorial, natural, mutually inverse or universal as appropriate.

(a)
[[aÞ b]] Bijectivity of l uses naturality and the two triangular laws. omitted diagram environment Naturality uses naturality (what else?). omitted diagram environment

(b)
[[bÞ c]] Putting l for B = F X, p = \idF X, u = \idX in Remark  7.2.3 gives omitted diagram environment so z mediates for l(z) and is unique because l is bijective ( cf the proof of the Yoneda Lemma, Theorem  4.8.12).

(c)
[[cÞ a]] First we must define F functorially on maps and show that h is natural. Fu = l-1(u; hY): FX® F Y is the unique map making the square commute, but this square states naturality of h: omitted diagram environment For  u = id only F u = id will do, and similarly F(u;|) = F u;F | both fill in for the composite along the top ( cf Proposition  4.5.13). Putting eA = l-1( \idUA) immediately satisfies law R, but we have to show that it satisfies  L and is natural. omitted diagram environment The naturality square for e in the left-hand diagram commutes since both routes serve for l-1(U z) using universality of hUA. The right hand diagram (the L law) commutes by naturality of h with respect to hX and by the definition of eF X; the top composite (FhX;eF X) and id both serve for l-1(hX), so L holds.

The proofs of [bÞ d] and [dÞ a] are dual, ie they are obtained from [bÞ cÞ a] by interchanging the parameters and reversing the arrows. []

Reflections and representables   The equivalence amongst these four presentations explains how various other terminologies arise. Recall from Theorem  4.8.12(b) that the Yoneda embedding identifies X Î obS with \HX = S(-,X) in SetSop, cf S¯ x in Definition 3.1.7.

COROLLARY 7.2.10

(a)
F:S® A has a right adjoint iff for each A Î obA, the presheaf (contravariant functor, Example 4.4.2(g)) A(F(-),A ):Sop® Set is representable, by X = UA (Definition 4.8.13). Cf the representable lower set {X|F(X) £ A} in the proof of Theorem 3.6.9.

(b)
U:A® S is the inclusion of a reflective subcategory iff it is part of some adjunction whose co- unit is invertible (being mono suffices), cf closure operations (Section 3.7).

(c)
U is an equivalence functor iff it is part of a strong equivalence.

PROOF: The first part is immediate and the other two are similar to Lemma 7.1.5. Recall the characterisations of

• reflectivity, by hUA being invertible for each A Î obA;

• weak equivalence, by hX being invertible for each X Î obS;

• strong equivalence, by hX and eA both being invertible, for each X Î obS and A Î obA respectively (Definition 4.8.9(b)).

By the R law hUA is invertible iff UeA is; indeed the latter being mono suffices. This holds if e is mono because U, being a right adjoint, preserves limits (Theorem  7.3.5) and hence monos (Proposition  5.2.2(d)). Conversely if U is the inclusion of a reflective subcategory then it is full and faithful, so e is invertible. []

The natural bijection is a simple and symmetrical way of presenting an adjunction and remembering (in a subject with plenty of traps for the dyslexic) which is left and which is right. Although an ``intuitively'' natural construction usually turns out to be natural in the formal sense, Theorem  7.6.9 shows that naturality may be the point at issue. We saw in Remark 7.2.3 how checking it can be built into the idiom.

The formulation using representables shows how to generalise the notion of universal property, for example to that of Cn[]L.

REMARK 7.2.11 Let A and C be 2-categories. The isomorphism A(F(-),( = )) º C(-,U( = )) may be replaced by either a strong or a weak equivalence of hom-categories (Definition  4.8.9). The various forms are illustrated by C/at: this has limits, exponentials and coproducts in the `` isomorphism'' sense ( cf Exercise 4.49), but other colimits can only be defined by an adjoint correspondence which is an equivalence functor. These different situations are distinguished by referring to 2-limits, but bi-colimits. Definition  7.3.8 also gives a new kind of 2-limit. An even more general situation is where A and C are enriched, ie A(A,B) and C(X,Y) belong to some other category |[thick] such as AbGp [Kel82].

Adjunctions are more common than the newcomer to category theory might expect, and individual cases are correspondingly less remarkable. Not unusually they are produced like a rabbit out of a hat, following an argument in which the more canny reader has watched the conjurer stuffing them in, as free algebras. The point is that, if the categories (S and A) and the functors (F and U) are artificial (A = SxS for the product, to give a mild example), then the significance of the adjunction F\dashv U is not particularly cogent. The universal property in the style of Definition 7.1.1 expresses the important facts more directly. It also avoids the question of Choice, which is, frankly, a red herring: this is a side-effect of imposing one-dimensional algebraic notation on a logical situation which is naturally a little subtler.