Lambek and Scott: Introduction to higher order categorical logic

Javascript Interactive Higher-Order Theorem Prover

Automated Reasoning in Higher Order Logic

This page was created and is maintained by Chad E Brown.

Lambek and Scott: Introduction to higher order categorical logic. (Available via Amazon)

1. Categories and functors. Concrete categories are structured sets and functions preserving the structure (we must, of course, have identities and compositions).

Slogan I. Many objects of interest in mathematics congregate in concrete categories.

A (directed) graph is a collection of arrows and a collection of objects with source (domain) and target (codomain) mappings. A deductive system is a graph with identity arros and composites (but no equations). A category is a deductive system with equations (satisfying identity and associativity laws).

Slogan II. Many objects of interest to mathematicians are themselves small categories.

Examples: Sets are discrete categories, monoids are categories with only one object, preorders are categories with each Hom set of cardinality at most 1.

A functor is a morphism of categories. When we consider sets, monoids, and preorders as categories, functors correspond to the appropriate notion of morphism.

Slogan III. Many objects of interest to mathematicians may be viewed as functors from small categories to Sets.

Examples: The category Sets corresponds to Sets^1. The category Graphs corresponds to Sets^{*=>*}. The category of M-sets (for a monoid M) corresponds to Set^M. (At this point we can only say the objects correspond, but soon the full functor categories are defined using natural transformations as arrows.)

From given categories we can define the opposite categories and product categories. Products are commutative and associative up to isomorphism.

2. Natural transformations. A natural transformation is a morphism between functors and give arrows in a functor category. We have certain natural isomorphisms of functor categories in Cat (the category of all categories). In particular, A^1 iso A, C^{A x B} iso (C^A)^B, (A x B)^C iso A^C x B^C.

Natural transformations compose with functors to give natural transformations. That is, given t:F->G for F,G:A->B, L:D->A, and K:B->C, we have KtL:KFL->KGL. Furthermore, given H:A->B and u:G->H, we have K(ut)L = (KuL)(KtL).

For a locally small category A, Hom:A^op x A -> Sets is a functor. The transpose of the Hom functor is Yoneda y:A -> Sets^{A^op} (or, Hom^*:A^op -> Sets^A). Each yA:A^op->Sets is a representable functor.

The Yoneda Lemma states that if A is locally small and F:A^op -> Sets is a functor, then Nat(yA,F) is isomorphic to the set FA (in fact, naturally in A and F). The actual isomorphism is important here: we send each a in FA to a~:yA->F by a~B:Hom(B,A)->FB by a~B(g:B->A) = F(g)(a). The inverse of this takes t:yA->F to tA(1) in FA.

The Yoneda Lemma is used to prove that the Yoneda functor is full and faithful. In fact, it is an embedding (injectivity on objects follows by simply noting that if yA = yB then 1_A is in H(A,A)=H(A,B) so that A=B). We have the functor is full and faithful since the arrow map y:Hom(A,A')->Nat(yA,yA') is, in fact, the Yoneda isomorphism. If you do not believe me, let f:A->A' and calculate for yourself: yf:yA->yA' (natural transformation) is given by yfB:Hom(B,A)->Hom(B,A') (set function) where yfB(g:B->A) = Hom(B,f)(g) = f o g. So what? Well, f~:yA->yA' was defined so that f~B:Hom(B,A)->yDB=Hom(B,A') by f~B(g:B->A) = yA'g(f) = Hom(g,A')(f) = f o g. Wow!

A very important application of this is that we can show C and D isomorphic in A (locally small) by showing yC is isomorphic to yD (since the isomorphism must be the image of an isomorphism in A). That is, we show Hom(X,C) isomorphic to Hom(X,D) naturally in X. You will use this application thousands of times throughout the rest of your life.

3. Adjoint functors. Functors between preorders are simply order preserving maps. Given preorders A and B and functors F:A->B and G:B->A, G is right adjoint to F iff Fa<=b iff a<=Gb for all a in A and b in B. (F,G) is called a Galois correspondence. In such a situation GF:A->A is a closure operation. That is, a<=GFa and GFGFa<=GFa (so GFGFa and GFa are isomorphic). Also, FG satisfies dual conditions and is an interior operation.

Given any Galois correspondence, we may pick the subpreorder of A of closed a (i.e., GFa is isomorphic to a) and subpreorder of B of open b (i.e., FGb is isomorphic to b). The Galois Correspondence (F,G) restricts to give an equivalence of these preorders. This principle is called the 'unity of opposites'.

Example: Letting A and B be the naturals (with the usual ordering), we can let F enumerate the primes (in order) and let G count the number of primes. It is easy to see that Fa<=b iff a<=Gb. The unity of opposites gives the isomorphism between the natural numbers and the primes.

Example: In propositional logic, given a fixed proposition B, the deduction theorem tells us "- and B" -| "B => -". The unity of opposites here is that propositions A such that |- A => B correspond to propositions A' such that |- (B => A') => A'.

Given any Galois correspondence (F,G), F preserves sups (special case of LAPC) and G preserves infs (special case of RAPL). Furthermore, we have the special case of Freyd's Adjoint Functor Theorem: If A and B are posets, A has sups, and F:A->B preserves sups, then it has a right adjoint G:B->A defined by G(b) = sup{a in A|Fa<=b}.

Of course, sometimes we are interested in F:A->B^op and G:B^op->A. Here a Galois correspondence gives b<=Fa iff a<=Gb.

Class of examples: For any binary relation R from X to Y, we have F:P(X)->P(Y)^op and G:P(Y)^op->P(X) so that B <= FA iff AxB <= R iff A <= GB. This is called a "polarity" and gives us an isomorphism between closed subsets of X and closed subsets of Y. Taking X to be the plane, Y to be the set of half-planes, and R to be membership, we have the closed subsets of X are the convex sets, and these correspond to the closed subsets of Y--the set of halfplanes containing the convex set. Closure (in X) takes a set to its convex hull.

For general categories A and B, an adjointness is (F,U,eta,eps) where F:A->B, U:B->A, eta:1_A->UF [unit], eps:FU->1_B [counit] satisfy the triangle equations Ueps o etaU = 1_U and epsF o Feta = 1_F. We write F -| U.

Equivalently, we can specify an adjointness by giving solutions to the universal mapping problem for a functor U:B->A (i.e., by giving an object F(A) in B and arrow eta(A):A->UF(A) so that for every f:A->U(B) there is a unique f*:F(A)->B such that f = U(f*) o eta(A).

Given any adjointness, we have an isomorphism of the Homs Hom(FC,D) and Hom(C,UD) given by U(-) o etaC and inverse epsD o F(-). A common way to show two arrows are equal is to apply one of these operators and show the results are equal.

Equations: Naturality of eps implies eps o epsFU = eps o FUeps. Naturality of eta implies etaUF o eta = UFeta o eta.

Examples: Free is left adjoint to forgetful (for algebraic varieties including monoids, groups, etc.). See also the list here.

A reflective subcategory B of A is a full subcategory so that the inclusion U:B->A has a left adjoint F:A->B. That is, for every object A, we have a "best approximation" FA and an arrow etaA:A->FA so that for every f:A->B there is a unique f*:FA->B such that f* o etaA = f. We say F is the reflector and eta is the reflection.

Example: Abelian groups and torsion free Abelian groups. FA is A/T(A) where T(A) is the torsion subgroup of A. For another example, consider Groups and Abelian groups. Here F'A is A/A' where A' is the commutator subgroup of A. We can even compose these and find that the category of torsion free Abelian groups is a reflective subcategory of the category of groups.

For locally small categories A and B, every adjointness gives rise to and determines a natural isomorphism between the functors Hom_B(F(-),-) and Hom_A(-,U(-)) from A^op x B to Sets.

Slogan IV. Many important concepts in mathematics arise as adjoints, right or left, to previously known functors.

Adjoints determine each other uniquely up to isomorphism and adjoints compose as in F-|U, F'-|U' give F'F-|UU' where F:A->B, F':B->C, U':C->B, U:C->A.

4. Equivalence of categories. An adjoint equivalence is an adjointness in which the unit and counit are natural isomorphisms. Equivalently, an equivalence is a pair of functors F:A->B and U:B->A with FU iso to 1_B and UF iso to 1_A.

Given any F-|U, we can take the full subcategories A_0B_0 of objects so that the components of eta and eps are isomorphisms. F and U restrict to these subcategories since if etaB:B->UFB is an isomorphism, then epsFB = inv(F(etaB)) by the triangle equation. Similarly, if epsA:FUA->A is an isomorphism, then etaUA = inv(U(epsA)) by triangle.

Also, note that if etaB:B->UFB is an isomorphism, then UFetaB = etaUFB (see this), and if epsA:FUA->A is an isomorphism, then FUepsA = epsFUA.

We also have etaU isomorphism iff epsF is. This follows from the equivalence of four statements:

The proof of (1) => (2) uses the naturality of eta to show that any left inverse of etaB is a right inverse (assuming 1!). Since the triangle equation gives a UepsB as a left inverse of etaUB, we have (2). The proof of (2) => (3) uses the fact that etaU o Ueps = 1 (this is NOT the triangle equation, but follows from it by the fact that etaU is an isomorphism) and the triangle equation epsF o Feta = 1. The rest of the theorem follows by duality.

If etaU and[equiv] epsF are isomorphisms, then the subcategory A_0 is reflective in A (with reflector UF) and B_0 is coreflective in B (with reflector FU). We can find the unique arrow f*:UFA->A' from f:A->A' so that f* o etaA = f as follows: By naturality of eta, we have UFf o etaA = etaA' o f. Since etaA' is invertible (A' is in A_0), we have inv(etaA') o UFf o etaA = f. So, let f* = inv(etaA') o UFf. Why is this unique?

Note that in some examples (such as - x B -| -^B) we only have the unit and counit being isomorphisms in the most degenerate cases.

Slogan V. Many equivalence and duality theorems in mathematics arise as an equivalence of fixed subcategories induced by a pair of adjoint functors.

5. Limits in categories. Terminal objects and products are examples of limits. Note that a terminal object can be characterized as a right adjoint: !:A->1 -| 1:1->A. Similarly, products can be characterized as right adjoints: K:A->AxA -| x:AxA -> A. Examples of colimits are initial objects and coproducts.

Equalizers give another example of a kind of limit. A result by Burroni allows us to characterize equalizers equationally (without conditions such as "if f=g, then we have . . ."). We can do this by taking for each f:A->B, delta(f):A->E(f,f), for all pairs B,g:A->B>, alpha(f,g):E(f,g)->A, and for each h:D->A, gamma(f,g,h):E(fh,gh)->E(f,g). The idea is that alpha gives the equalizer, gamma gives the UMP arrow (modulo delta and the condition that f o h = g o h), and delta provides an isomorphism between E(f,f) and the domain of f. These should satisfy the following equations:

In B4, beta(f,g,h) is defined by gamma(f,g,h) o delta(f o h). So, the idea is that when f o h = g o h, then we have alpha(f,g) o beta(f,g,h) = alpha(f,g) o gamma(f,g,h) o delta(f o h) = h o alpha(f o h,g o h) o delta(f o h) = h. So, beta(f,g,h) is the arrow whose unique existence is guaranteed by the universal mapping property of equalizers. When we do not know f o h = g o h, we can still form alpha(f,g) o beta(f,g,h), but we cannot conclude that it equals h.

In general, we can start with a category A and a (small) index category I. An I-diagram is a functor D:I->A. A limit of the diagram D is a terminal object in the category of pairs (A,t) with A in A and t:KA->D a natural transformation where K:A->A^I (given by KAi = A) is the constancy functor. Colimits are defined to be an initial object in the category of pairs (A,t:D->KA).

A category A has all I-limits [I-colimits] iff the constancy functor K:A->A^I (given by KAi = A) has a right adjoint L:A^I->A [left adjoint C:A^I->A]. The idea is that for any "diagram" D:I->A (or Gamma:I->A if you like), LD gives the limit of D. But we should be careful. We often talk about the object LD of A as the limit, when in actuality it is the object LD and the counit eps:KLD->D that form the limiting cone. (For each object i of I, epsi:LD->Di, and the family satisfies epsj = Da o epsi for every a:i->j in D.) Cones correspond to arrows KB->D in A^I. The adjunction tells us that for any t:KB->D, there is a unique t*:B->LD (arrow in A) such that eps o K(t*) = t. (So, for each i, epsi o t* = ti.)

Covariant Representable Functors Preserve Limits. For a locally small category A, the functor Hom(A,-):A->Sets preserves limits. We can check this directly by showing Hom(A,lim(Gamma)) gives a limit for Hom(A,-) o Gamma:I->Sets. Okay, let's be very precise and careful about what we're saying. Start with Gamma:I->A. Suppose we have limit (A0,t0:K(A0)->Gamma). Let's write hA for Hom(A,-). So, hA:A->Sets. Composing we have the diagram hA o Gamma:I->Sets. A limit of this diagram in Sets is a terminal pair (S,s:KS->hA o Gamma) where S is a set and for each i in I, si:S->Hom(A,Gamma(i)) is a function. We can show that (hA(A0),hA o t0:hA o K(A0)->hA o Gamma) (that is, (Hom(A,A0),s0:K(Hom(A,A0))->hA o Gamma) where s0 = hA o t0 and we notice (hA o K(A0))(i) = Hom(A,A0) = K(Hom(A,A0))) is such a terminal pair.

Here is the check: Given any (S,s:KS->hA o Gamma), we need to show there is a unique function psi:S->Hom(A,A0) such that for every i in I, si = s0i o psi:S->Hom(A,Gamma(i)). For this equation to hold for every i, we need si(x) = t0i o psi(x) to hold for every i in I and x in S. Well, fix x in S. Now, we have a cone (A,sx:KA->Gamma) for Gamma and so we have a unique psi(x):A->A0 so that si(x) = sxi = t0i o psi(x) = Hom(A,t0i)(psi(x)) = ((hA o t0)i o psi)(x). This defines psi uniquely for each x and we have si = (hA o t0) o K(psi).

So, let's say what we really mean by a functor F:A->B "preserves limits". Usually we naively write something like F(lim(Gamma)) = lim(F o Gamma), but there's a bit more to it than this. lim(Gamma) = (A,t:KA->Gamma). And lim(F o Gamma) = (B,u:KB->F o Gamma). So, what we're saying is FA = B and F o t = u. That is, writing lim(Gamma) = (lim1(Gamma),lim2(Gamma)), we have F preserves limits if F(lim1(Gamma)) = lim1(F o Gamma) and F o lim2(Gamma) = lim2(F o Gamma). Of course, I'm writing =, but what I mean is that (F(lim1(Gamma)),F o lim2(Gamma)) is a limit of F o Gamma.

Right adjoints preserve limits (RAPL) and left adjoints preserve colimits. If A and B are locally small, then we can show this for F:A->B -| U:B->A and Gamma:I->B by using the fact that covariant representable functors preserve limits: Hom(-,lim(U o Gamma)) iso lim(Hom(-,U(Gamma-))) by above; Hom(-,U(Gamma-)) iso Hom(F-,Gamma-) by the adjunction; lim(Hom(F-,Gamma-)) "is" Hom(F-,lim(Gamma)) by above; Hom(F-,lim(Gamma)) iso Hom(-,U(lim(Gamma))) by the adjunction; so Hom(-,lim(U o Gamma)) iso Hom(-,U(lim(Gamma))); since Yoneda is an embedding lim(U o Gamma) iso U(lim(Gamma)) in A. Okay, that's the informal idea. I would prefer to say this, as in the last paragraph:

y(lim1(U o Gamma)) = lim1(y(-,U o Gamma)) = lim1(Hom(F-,Gamma-)) = Hom(F-,lim1(Gamma)) = Hom(-,U(lim1(Gamma)))

6. Triples. Triples are monads. A monad on a category A is a functor T:A->A and two natural transformations eta:1->T and mu:T^2->T satisfying two unit laws and an associative law:

A result attributed to Huber tells us that every adjointness (F,U,eta,eps) gives a monad (UF:A->A,eta,UepsF). The unit laws follow from the triangle equations. The associative law follows by naturality of eta.

Conversely, every monad can be represented by adjoints in this way. Many adjoints will do the job. In fact, we can build a category of resolutions: A resolution of a monad (T,eta,mu) is (B,U,F,eps) where (U,F,eta,eps) is an adjointness and we have T=UF and mu=UepsF. The arrows are functors Phi from B to B' which respect the functors U and F and transformation eps (U'Phi = U, PhiF = F', Phi(eps) = eps'Phi).

Two particular resolutions of interest are constructed from the Eilenberg-Moore category and from the Kleisi category. The Eilenberg-Moore category gives rise to a terminal resolution. The Kleisi category gives rise to an initial resolution.

The Eilenberg-Moore Category. The objects of this category A^T are T-algebras, where (T,eta,mu) is a monad (T:A->A). A T-algebra is a pair (A,phi:TA->A) where A is an object in A satisfying two conditions:

An arrow (a homomorphism of T-algebras) is an arrow a:A->A' in A so that phi' o Ta = a o phi.

We let U:A^T->A be U(A,phi) = A and Ua = a. (U forgets structure, as many right adjoints do.) Clearly, U is a faithful functor.

We let F:A->A^T be FA = (TA,mu_A) and Fa = Ta. The fact that (TA,mu_A) is a T-algebra follows from the unit laws and associative law for monads. The fact that Ta:(TA,mu_A)->(TA',mu_A') is a T-algebra homomorphism follows from naturality of mu.

We let eps:FU->1 be given by eps(A,phi) = phi:(TA,mu_A)->(A,phi). This is a T-algebra homomorphism for each (A,phi) by the mu equation in the definition of T-algebras. We can show eps is natural (eps(A',phi') o FUa = phi' o Ta = a o phi = a o eps(A,phi) for a:(A,phi)->(A',phi')) using the fact that a is a T-algebra homomorphism.

This does give a resolution since T=UF and UepsF = mu (since UepsFA = Ueps(TA,mu_A) = U(mu_A) = mu_A).

To see that this is terminal in the category of resolutions, suppose we have a resolution (B,U',F',eps'). We need to show there is a unique functor K:B->A^T such that UK = U', KF' = F, and Keps' = epsK. For each object B in B, KB should be a T-algebra. To have UK = U', we must let the object of the T-algebra KB be U'B (object in A). For each arrow b:B->B' in B, Kb should be a T-algebra homomorphism. UK = U' also forces us to take Kb = U'b. To have Keps' = epsK, we must let the map phi:TU'B -> U'B (or phi:U'F'U'B->U'B) of the T-algebra KB be U'(eps'_B). (Why? Because epsKB is the map phi of the T-algebra homomorphism KB by definition. And K(eps'_B) = U(eps'_B) by the forced definition of K on arrows.)

So, to sum up, the only possible functor that could work is defined to take KB = (U'B,U'(eps'_B)) and Kb = U'b. To check this does define a functor, note that (U'B,U'(eps'_B)) defines a T-algebra by T=U'F', one of the triangle equations (for eps' and eta'), and naturality of eps'. Also, U'b:(U'B,U'(eps'_B))->(U'B',U'(eps'_B')) is a T-algebra homomorphism naturality of eps'. Finally, this is a functor since U' is a functor. This K is called the comparison functor.

A functor U:B->A is called "tripleable" or "monadic" if it is a right adjoint and if the comparison functor is an equivalence of categories (so that up to equivalence B is the Eilenberg-Moore category).

The Kleisi Category. The objects of this category A_T are the same as the objects of A, but an arrow from A to A' is an arrow f:A->T(A') in A. We compose f:A->T(A') and g:A'->T(A'') by taking g*f = mu_A'' o T(g) o f. eta_A is the identity arrow at A by the monad unit laws and naturality of eta: eta_A * f = mu_A o T(eta_A) o f = f and f * eta_A = mu_A o T(f) o eta_A = mu_A o eta_TA o f = f. Composition is associative by the associative law of monads and naturality of mu: (h*g)*f = mu_A''' o T(mu_A''' o T(h) o g) o f = mu_A''' o T(mu_A''') o TTh o Tg o f = mu_A''' o mu_TA''' o TTh o Tg o f = mu_A''' o Th o mu_A'' o Tg o f = h*(g*f).

The Kleisi category gives rise to an initial resolution of the monad as follows:

Let U:A_T->A be given by UA = TA and U(f:A->TB) = mu_B o Tf. U(eta_A) = mu_A o T(eta_A) = 1_A by a unit law of monads. Also, using the associativity law for monads and the naturality of mu we have, U(g*f) = mu_C o T(mu_C o Tg o f) = mu_C o Tmu_C o TTg o Tf = mu_C o mu_TC o TTg o Tf = mu_C o Tg o mu_B o Tf = U(g) o U(f). So, U is a functor.

Let F:A->A_T be given by FA = A and F(f:A->B) = eta_B o f. Note that F is bijective on objects. F(1_A) = eta_A. Also, by one of the monad unit laws (again!) and naturality of eta, we have F(g)*F(f) = mu_C o T(eta_C o g) o eta_B o f = mu_C o T(eta_C) o Tg o eta_B o f = Tg o eta_B o f = eta_C o g o f = F(g o f). So, F is a functor.

It is easy to see that T = UF. On arrows we have UF(f) = mu_B o T(eta_B o f) = mu_B o Teta_B o Tf = Tf.

Now, eps:FU->1 should be a family of arrows eps_A from FUA=TA to A in A_T. That is, an A-arrow from TA to TA. So, let eps_A = 1_TA. Naturality follows by f * eps_A = mu_B o Tf o 1_TA = mu_B o Tf = mu_B o 1_TB o Tf = eps_B * Tf.

By a unit law for monads, Ueps_A o eta_UA = mu_A o T(1_TA) o eta_TA = mu_A o eta_TA = 1_TA.

Using the same unit law for monads again, we have eps_FA * Feta_A = mu_A o T(1_TA) o eta_TA o eta_A = mu_A o eta_TA o eta_A = eta_A.

So, we do have an adjunction. To check mu = UepsF, calculate: UepsFA = U(1_TA) = mu_A o T(1_TA) = mu_A. So, we in fact have a resolution of the monad.

Why is this initial? Suppose we have another resolution (B,U',F',eps'). We need to show there is a unique K:A_T->B such that U'K = U, KF = F', and Keps = eps'K. To have KF = F', we must have KA = F'A. To have Keps = eps'K, we must have K(1_TA) = Keps_A = eps'_KA = eps'_F'A. (If you think K(1_TA) = 1_KTA, think again. 1_TA is not the identity arrow on TA in A_T-- eta_TA is.) So, we know K(1_TA) = eps'_F'A. Now, given any arrow g:A->TA' in A (i.e., arrow g:A->A' in A_T), we can determine K(g) using KF = F' as follows. First, 1_TA' * (eta_TA' o g) = mu_A' o T(1_TA') o eta_TA' o g = mu_A' o eta_TA' o g = g. Now, using g = 1_TA' * (eta_TA' o g), KF = F', K(1_TA') = eps'_F'A', the definition of F, and the functorial properties of K, we have K(g) = K(1_TA' * (eta_TA' o g)) = K(1_TA') o K(eta_TA' o g) = eps'_F'A' o K(F(g)) = eps'_F'A' o F'(g). So, after pulling it all together, we are forced to define K(g) = eps'_F'A' o F'(g).

So, KA = F'A, and K(g:A->TA') = eps'_F'A' o F'(g). It remains to show this is a functor and it respects resolutions.

K is a functor since K(eta_A) = eps'_F'A o F'(eta_A) = 1_A, and K(g*f) = eps'F'A'' o F'(mu_A'' o T(g) o f) = eps'F'A'' o F'U'eps'F'A'' o F'U'F'g o F'f = eps'F'A'' o eps'F'U'F'A'' o F'U'F'g o F'f = eps'F'A'' o F'g o eps'F'A' o F'f = K(g) o K(f).

We made sure K satisfied KF = F' by the way we constructed it, but just to double-check for f:A->A', calculate: KF(f) = K(eta_A' o f) = eps'_F'A' o F'(eta_A' o f) = eps'_F'A' o F'eta_A' o f = f. (Do not be confused by the fact that eps' has a prime and eta does not. There are potentially different counits epsilon for each resolution, but there is only one unit eta which comes from the fixed monad.)

We also made sure K satisfied Keps_A = eps'_KA by the construction of K, but again to double check, note that Keps_A = K(1_TA) = eps'_F'A o F'(1_TA) = eps'_F'A = eps'_KA.

To check U'K=U, first check U'KA = U'F'A=TA=UA. Now, for g:A->TA' (i.e., g:A->A' in A_T), U'Kg = U'(eps'_F'A' o F'g) = U'eps'F'A' o U'F'g = mu_A' o Tg = Ug.

We can use the results above to embed the Kleisi Category of a monad into the Eilenberg-Moore Category of the monad. We know there is a unique functor L:A_T->A^T which satisfies (writing ^T for the adjunction components of the Eilenberg-Moore resolution and _T for the adjunction components of the Kleisi resolution) F^T = L o F_T, U_T = U^T o L, and L(eps_T) = eps^T_L. So, from F^T -| U^T, we have L o F_T -| U^T. Also, from F_T -| U_T, we have F_T -| U^T o L. We also recall that F_T is bijective on objects and U^T is faithful.

We can also show that L is full and faithful. To do this, we must recall how the comparison functor L (or, K^T) was defined in the proof that the Eilenberg-Moore resolution is terminal. For an arrow g:A->TA' in A (arrow g:A->A' in A_T), Lg = U_T(g) (U_T was the general U' in the proof). Now, we recall how U_T was defined in the construction of the Kleisi resolution and obtain Lg = U_T(g) = mu_A' o Tg. We need to show, for fixed A and A', that this map of arrows is bijective. We invert the map as follows: Lg o eta_A = mu_A' o Tg o eta_A = mu_A' o eta_TA' o g = g using naturality of eta and a monad unit law.

L tells us that the Kleisi category is equivalent to a full subcategory of the Eilenberg-Moore category. If we look at the actual images of objects under L, we find that LA = = = . These are the 'free' T-algebras. So, the Kleisi category is equivalent to the full subcategory of the Eilenberg-Moore category consisting of all free T-algebras. It makes sense to all these the free T-algebras because they are the images under F^T, which is right adjoint to U^T, and it is clear how to view U^T as forgetful.

M-sets Example. Given a monoid M, we can form that monad T:Sets->Sets given by T(-)=M x - with eta_A:A->MxA by eta_A(a)=(1,a) and mu_A:Mx(MxA)->MxA by mu_A(m1,(m2,a))=(m1.m2,a). The unit laws and associative law for monads follows from the corresponding laws for the monoid M.

The Kleisi category has arrows f:A->MxB. The identity eta_A:A->MxA takes a to (1,a). Composition of f:A->MxB and g:B->MxC is g*f:A->MxC taking g*f(a) = (g(f(a)_2)_1.f(a)_1,g(f(a)_2)_2). By the discussion above, we know this category is equivalent to the full subcategory of M-sets consisting of the "free" M-sets. If we instantiate what we mean by "free" M-sets, we find they are the M-sets of the form .

Covariant Power Set Example. Let P:Sets->Sets be the functor taking A to the power set PA, and f:A->A' to the image function Pf:PA->PA'. We obtain a monad by letting eta_A(a)={a} and mu_A(X) = Union(X). Checking the unit and associative laws is a naive set theory exercise.

The T-algebras here are phi:PA->A with phi({a})=a and phi(Union(X))=phi({phiX|X in X}). Now, in the book they say the algebras are "sup-complete lattices". Do these look like sup-complete lattices to you? Well, they didn't to me, but fortunately I worked out the details one night in December, 1998, in Wean 7220. (Like many problems in mathematics, it turns out to be simple when you look at it in the right way.) It also turns out that the T-algebra homomorphisms correspond to sup preserving mappings.

The Kleisi Category is much simpler. Arrows are of the form f:A->P(B) which correspond in an obvious way to relations R_f from A to B. The identity at A is eta_A(a)={a} and corresponds to the identity relation on A. Composition of f:A->P(B) and g:B->P(C) is given by g*f(a)=Union({g(b)|b in f(a)}). The corresponding relation between A and C relates a to c iff there is a b in B with (a,b) in R_f and (b,c) in R_g. This is the usual notion of composition of relations. So, the Kleisi Category of this monad is isomorphic to the category of sets and relations.

Slogan VI. Many categories of interest are the Eilenberg-Moore categories of triples on familiar categories.

7. Examples of cartesian closed categories. A category with finite products (including a terminal object) is cartesian closed if for every B, -xB has a right adjoint -^B. Examples include Sets, presheaf categories (Sets^X for small categories X), any topos, and so on.