In the previous post I explored the application of the Yoneda lemma in the functor category to derive some results from the Haskell lens library. In particular I derived the profunctor representation of isos. There is one more trick that is used in the lens library: combining the Yoneda lemma with adjunctions. Jaskelioff and O’Connor used this trick in the context of free/forgetful adjunctions, but it can be easily generalized to any pair of adjoint higher order functors.

An adjunction between two functors, `L` and `R` (left and right functor) is a natural isomorphism between hom-sets:

`C(L d, c) ≅ D(d, R c)`

The left functor `L` goes from the category D to C, and the right functor `R` goes in the opposite direction. Formally, having an adjunction allows us to shift the action of the functor from one end of the hom-set to the other. The shortcut notation for an adjunction is `L ⊣ R`.

Since adjunctions can be defined for arbitrary categories, they will also work between functor categories. In that case objects are functors and hom-sets are sets of natural transformations. For instance, Let’s consider an adjunction between two higher order functors:

```ρ :: [C, C'] -> [D, D']
λ :: [D, D'] -> [C, C']```

Here, `[C, C']` is a category of functors between two categories C and C’, `[D, D']` is a category of functors between D and D’, and `ρ` maps functors (and natural transformations) between these two categories. `λ` goes in the opposite direction. The adjunction `λ ⊣ ρ` is expressed as a natural isomorphism between sets of natural transformations:

`[C, C'](λ g, h)  ≅  [D, D'](g, ρ h)`

The two objects in functor categories are themselves functors:

```h :: C -> C'
g :: D -> D'```

Here’s the same adjunction written using ends:

`∫x∈C C'((λ g) x, h x)  ≅  ∫y∈D D'(g y, (ρ h) y)`

The end notation is easily translatable to Haskell. The end corresponds to a universal quantifier `forall`, and hom-sets become function types:

`forall x. (lambda g) x -> h x ≅ forall y. g y -> (rho h) y`

Since `lambda` and `rho` act on functors, they have kinds `(*->*)->(*->*)`.

Let’s recall the formula for the Yoneda embedding of the functor category:

```∫f Set(∫x D(g x, f x), ∫y D(h y, f y))
≅ ∫z D(h z, g z)```

Here, `g`, `h`, and `f`, are functors — objects in the functor category `[C, D]`. The ends represent natural transformations — morphisms in the functor category. The end over `f` is a higher order natural transformation.

Since `g` and `h` are arbitrary, let’s replace them with the results of the action of some higher order functors, `λ g` and `λ' h`. The idea is that `λ` and `λ'` are left halves of some higher order adjunctions.

```∫f Set(∫x D'((λ g) x, f x), ∫y D'((λ' h) y, f y))
≅ ∫z D'((λ' h) z, (λ g) z)```

The right halves of these adjunctions are, respectively, `ρ` and `ρ'`.

```λ  ⊣ ρ
λ' ⊣ ρ'```

Let’s apply these adjunctions inside the hom-sets:

```∫f Set(∫x D(g x, (ρ f) x), ∫y D(h y, (ρ' f) y))
≅ ∫z D(h z, (ρ' (λ g)) z)```

Let’s focus our attention on the category of sets. If we replace D with Set, we can pick `g` and `h` to be hom-functors (which are the simplest representable functors) parameterized by some arbitrary objects `b` and `t`:

```g = C(b, -)
h = C(t, -)```

We get:

```∫f Set(∫x Set(C(b, x), (ρ f) x), ∫y Set(C(t, y), (ρ' f) y)
≅ ∫z Set(C(t, z), (ρ' (λ C(b, -))) z)```

Remember, hom-functors behave like Dirac delta functions under the integration sign. That is to say, we can use the Yoneda lemma to “integrate” over `x`, `y`, and `z`:

```∫f Set((ρ f) b, (ρ' f) t)
≅ (ρ' (λ C(b, -))) t```

We are now free to pick a pair of adjoint higher order functors to suit our goal. Here’s one such choice for `ρ`: the functor that maps a functor `f` (an endofunctor in C) to a set of morphisms from some fixed object `a` to `f` acting on another object. This is an operation that lifts a functor to a profunctor. In Haskell it’s defined as `UpStar`. This higher-order functor is parameterized by the choice of the object `a` in C:

`κa f = C(a, f -)`

It can also be written in terms of the exponential object:

`κa f = (f -)a`

This functor has an obvious left adjoint:

`λa g = a × g -`

This follows from the standard adjunction between the product and the exponential.

Our pick for `ρ'` is the same functor but taken at a different carrier, `s`:

`ρ' = κs`

With those choices, the left side of the identity

```∫f Set((ρ f) b, (ρ' f) t)
≅ (ρ' (λ C(b, -))) t```

becomes:

`∫f Set(C(a, f b), C(s, f t))`

This is the categorical version of the van Laarhoven lens.

Let’s now evaluate the right hand side. First we apply `λa` to the hom-functor `C(b, -)` to get:

`λa C(b, -) = a × C(b, -)`

The action of `ρ'` produces the result:

`C(s, (a × C(b, t)))`

This, in turn, is the categorical version of the getter/setter representation of the lens.

## Translation

In Haskell, our formula derived from the higher-order Yoneda lemma with the adjoint pair:

```∫f Set((ρ f) b, (ρ' f) t)
≅ (ρ' (λ C(b, -))) t```

takes the form:

```forall f. Functor f => (rho f) b -> (rho' f) t
≅ (rho' (lambda ((->)b))) t```

With our choice for `ρ` as the up-star functor:

```rho  f = a -> f -
rho' f = s -> f -```

```type Rho  a f b = a -> f b
type Rho' s f t = s -> f t```

we get:

```forall f. Functor f => (a -> f b) -> (s -> f t)
≅ (rho' (lambda ((->)b))) t```

To get the `λ`, we plug our `ρ` into the adjunction formula. We get:

`forall x. (lambda g) x -> h x ≅ forall x. g x -> a -> h x`

which has the obvious solution:

`lambda g = (a, g -)`

`type Lambda a g x = (a, g x)`

Indeed, with the currying and flipping of arguments, we get the adjunction:

`forall x. (a, g x) -> h x ≅ forall x. g x -> a -> h x`

Now let’s evaluate the right hand side:

`(rho' (lambda ((->) b))) t`

`lambda (b -> -) = (a, b -> -)`

The action of `rho'` gives us:

`rho' (a, b -> -) = s -> (a, b -> -)`

Altogether:

`(rho' (lambda ((->) b))) t = s -> (a, b -> t)`

So the right hand side is just the getter/setter pair:

`(s -> a, s -> b -> t)`

The final result is the well known van Laarhoven representation of the lens:

```forall f. Functor f => (a -> f b) -> (s -> f t)
≅ (s -> a, s -> b -> t)```

This is not a new result, but I like the elegance of this derivation — especially the role played by the exponential adjunction and the lifting of a functor to a profunctor. This formulation has the additional advantage of being generalizable towards the profunctor formulation of lenses.