Given these two facts, we can speedily derive that a right adjoint preserves limits:
```
Hom_C(a:C , R(lim F: J -> D)): Set
= Hom_D(L(a), lim F: J -> D) [Adjunction]
~= {lim (\j. Hom_D(L(a), F(j)): J -> Set}: Set [Hom lim = lim Hom]
~= {lim (\j. Hom_C(a, R(F(j)))): J -> Set}: Set [Adjunction inside lim]
~= Hom_C(a, {\j. R(F(j))}: J -> C): C [lim Hom = Hom lim]
~= Hom_C(a, R . F)
```

#### § `Hom(a, -)`

preserves limits:

We wish to show that the `Hom(a, -)`

functor preserves limits. That is:
```
Hom(a, lim F: J -> C): Set ~= lim(\j. Hom(a, F(j)): J -> Set): Set
```

Let's start with `Hom(a, lim F: J -> C): Set`

. An element of this
is a morhism `arr: a -> lim F`

from `a`

to the apex
of the limit cone `lim F`

. We need to translate this into a `lim(\j. Hom(a, F(j)): J -> Set): Set`

,
which is a family of morphisms from each `a`

to each `{ F(j) : j in J}`

. This is obtained
by composing the projection maps `pi(j): lim F -> F(j)`

with `arr: a -> lim F`

to
get `pi(j) . arr : a -> F(j)`

which lives in `Hom(a, F(j))`

. We get the limit by considering
the family of these maps, as the Limit in `Set`

is just a product with coherence conditions,
and an element of the limit is a tuple/family with coherence conditions.
To go the other way around, suppose we have an element in the limit
`lim(\j. Hom(a, F(j)): J -> Set): Set`

. This means that we have a family of maps from `a`

to `F(j)`

which obeys the coherence conditions. This means that `a`

is the apex of some valid cone. But we
know that `lim F`

is the universal cone, thus the `a`

cone must factor through `lim F`

. This gives
us a factoring map `factor: a -> lim F`

. The map `factor`

lives in `Hom(a, lim F)`

. This gives the other
way round.
Thus, the two sets are equivalent, and hence `Hom(a, -)`

preserves limits (almost by definition).