Two functors that
almost invert

Picture two categories: C on the left, D on the right. Now picture two functors going between them — one each way:

• F : C → D  — takes objects of C, builds objects of D out of them.
• G : D → C  — takes objects of D, gives back something in C.

Most of the time these two don't fit together at all. But sometimes — surprisingly often — they fit together in a special, precise way. We say F is left adjoint to G (and G is right adjoint to F) and we write it like this:

F ⊣ G

The mental picture worth carrying: F builds something freely (adds structure in the most efficient way possible, no extra commitments), and G forgets something (throws structure away to land back in a simpler category). They go in opposite directions and they almost — but not quite — undo each other.

Here's the soul of the definition, in plain English first. Pick any object c in C and any object d in D. Now look at two sets of arrows:

• arrows in D that go out of F(c) and into d,
• arrows in C that go out of c and into G(d).

The promise of an adjunction is: these two sets of arrows are in one-to-one correspondence. Every arrow F(c) → d over in D corresponds to exactly one arrow c → G(d) back in C, and vice versa. Read it as a slogan:

an arrow out of F(c)  =  an arrow into G(d)

And one technical refinement: the correspondence has to be natural in both c and d — meaning, in the spirit of Ch.5, it commutes with whatever pre- or post-composition you might want to do. The bijection isn't ad-hoc per pair of objects; it's a single, uniform mechanism that works for every pair at once.

Only now do we write the formal version. Using the notation D(x, y) for "the set of arrows from x to y in category D":

D(F(c), d)  ≅  C(c, G(d))

That's it. That tidy line is the entire defining property of an adjunction. The rest of this chapter is unpacking what it does for you.

Time to make this concrete. Here's the cleanest example in all of programming.

You have a plain set A — say, the three letters {a, b, c}. You want a monoid that contains those letters. (A monoid, recall, is a set with an associative combine and an empty element.) What's the smallest, cheapest monoid you can possibly build that has those letters in it?

You make sequences. You can put one letter, or two, or seventeen, in a row. You can concatenate two sequences. The empty sequence is the empty element. That's the free monoid on A. And in code, it's just List[A], with concatenation as combine and the empty list as the empty element.

Now name the two categories:

• Set — sets and ordinary functions between them.
• Mon — monoids and monoid homomorphisms (functions that respect combine and empty).

And the two functors going between them:

• Free : Set → Mon  — takes a set A and gives back List[A], the free monoid on A.
• U : Mon → Set  — the forgetful functor. Takes a monoid and throws away the combine and empty operations — keeps just the underlying set of elements.

The claim: Free ⊣ U. The bijection says:

Mon( Free(A), M )  ≅  Set( A, U(M) )

In English: a monoid homomorphism out of List[A] into a monoid M is exactly the same data as an ordinary function from A into the underlying set of M. You only have to say where the generators go. The list structure — concatenation, empty — forces the rest. Try the widget below.

Back in Chapter 9 you met currying: the bijection that turns a function of two arguments into a function returning a function. It turns out that's not just a bijection — it's an adjunction.

Fix some type A. Consider two functors on the category of types:

• - × A  — "pair me up with an A." Takes a type B to the product type B × A.
• (-)^A  — "function from A into me." Takes a type C to the function type A → C.

The claim: (- × A) ⊣ ((-)^A). Spell out the bijection:

Hom(B × A, C)  ≅  Hom(B, C^A)

In programmer terms: (B × A) => C  is the same data as  B => (A => C). The bijection going one way is curry; going the other way is uncurry. The very definition of an exponential — the universal property that pins down function types — is this adjunction.

The bijection in section 2 is the slickest way to state an adjunction, but there's an equivalent formulation that's more useful day-to-day. Every adjunction comes with two natural transformations (Ch.5 vocabulary). Plain English first:

• The unit, written η, is the "embed me into the round trip" map. For each object c in C, it gives you an arrow c → G(F(c)). Start in C, ride F over to D, ride G back to C, and the unit is the natural way you got there.
• The counit, written ε, is the "extract me from the round trip" map. For each object d in D, it gives you an arrow F(G(d)) → d. Start in D, ride G back to C, ride F forward to D, and the counit is the natural way you collapse back.

Notice the shape — neither is an identity. η doesn't say "the round trip is the identity," it just gives you a comparison arrow to the round trip. That's the almost in "almost invert."

Made concrete on Free ⊣ U

• Unit η : A → U(Free(A)) = List[A]  is a => List(a). The "singleton list" function. It embeds each generator into the freely-built list.
• Counit ε : Free(U(M)) → M  is "fold this list with M's combine, starting from M's empty." It collapses a list of monoid elements down into a single monoid element. (In Scala: _.fold(M.empty)(M.combine).)

Look closely at the counit's name in code: it's just fold. The counit of the free-monoid adjunction is fold. That tells you why fold is so central — it's the unique structure-collapsing map handed to you by the universal property.

Here's the big payoff — the punchline that took twelve chapters to set up.

Every adjunction gives you a monad.

Given F ⊣ G between C and D, look at the composite functor G ∘ F : C → C. It goes from C to D and right back to C. That composite is the underlying functor of a monad on C. And the monad's two operations — pure and flatMap (the "return" and "bind" from Ch.6) — are built directly from the unit and counit:

• pure  = the unit  η : c → G(F(c)). It lifts a plain value into the monadic context.
• flatMap  uses the counit ε applied at F(c), sandwiched with G, to collapse a nested context.

Take this seriously: every monad you have ever used in code comes from an adjunction. The List monad is the monad of the Free ⊣ Forgetful adjunction between Set and Mon. The State monad comes from a currying-style adjunction. The Maybe monad comes from the adjunction that freely adds a "nothing" element. The Reader monad comes from a different currying adjunction. Every single one has an adjunction hiding inside it.

Back in Chapter 8 we met Galois connections: pairs of monotone functions f : P → Q and g : Q → P between two ordered sets, with the wonderful property

f(p) ≤ q   ⟺   p ≤ g(q)

Stare at that ⟺. Now compare it to the adjunction bijection from section 2:

D(F(c), d)  ≅  C(c, G(d))

In a poset there's at most one arrow between any two objects (the ≤ either holds or doesn't). So the bijection between sets of arrows collapses to a bijection between two facts — i.e., to a logical equivalence. The ≅ becomes ⟺. A Galois connection IS an adjunction in a poset. You were doing adjunctions the whole time and you didn't know it.

Look back. In Chapter 1 we said the essence is composition — arrows you can chain. By Chapter 6 we had monads: arrows that drag a context along with them, so you can chain context-aware computations. Chapter 7 reframed monads as categories — the Kleisli category, where composition gives you sequencing for free. Chapter 8 showed that orders are categories too, dressed down to their bones. Chapter 9 introduced exponentials and first-class functions. Chapter 10 showed every recursive type folds the same way — F-algebras and catamorphisms. Chapter 11 said you are completely determined by what you map into — the Yoneda lemma.

And here, at Chapter 12: the things in those eleven chapters aren't eleven different ideas. They're one idea — adjunction — in eleven disguises. Monads? An adjunction with itself folded down. Currying? An adjunction. Galois connections? An adjunction. Free constructions? An adjunction. Limits and colimits, which we touched on with products and coproducts, are characterized by adjunctions too. Catamorphisms? Universal maps out of free algebras — adjunctions in another costume.

The reason category theory feels like it explains so much with so little is that the same handful of universal patterns recur everywhere. Adjunction is the most universal of them all. You have now seen what the whole course was pointing at.

An Adjunction[F, G] in code is precisely the bijection: a pair of inverse functions leftAdjunct and rightAdjunct. Below: the curry/uncurry adjunction made literal, and a sketch of how it spits out a monad. Same code in Scala and Haskell.

From a single "do nothing" arrow on a single object, all the way here. Twelve chapters, one through-line: arrows you can compose, and the universal patterns that arrows can satisfy.

Composition (Ch.1) gave you the engine. Types & functions (Ch.2) named the things. Products & coproducts (Ch.3) gave you the algebra of bundling and choice. Functors (Ch.4) lifted arrows into contexts. Natural transformations (Ch.5) translated between contexts. Monads (Ch.6) sequenced them. Kleisli (Ch.7) reframed monads as categories. Orders (Ch.8) revealed posets as categories too. Function types (Ch.9) gave you the exponential. F-algebras (Ch.10) gave you the universal fold. Yoneda (Ch.11) said an object is its arrows. And adjunctions (Ch.12) showed that all of those are one shape in many disguises.

That is the programmer-facing core of category theory. Use it well — and look for adjunctions in the wild. They are everywhere.