§ Working out why right adjoints preserve limits.

We have L: C -> D and R: D -> C adjoints functors, so we have the condition:
  1. Hom(L(a): D, b: D) ~= Hom(a: C, R(b): C)
We will also show that Hom(A, -) preserves limits: 
Hom(a, lim (F: J -> C):C) : Set ~= lim ({Hom(a, -) . F}: J -> Set): Set
 Hom(a, lim (F: J -> C):C) : Set ~= lim (\j. Hom(a, F(j)): J -> Set): Set
The above statement, fully elaborated with all the types looks as follows: 
lim :: (J -> K) -> K
Hom(a: C, {lim (F: J -> C)}:C ): Set ~=
lim (\j. Hom(a, F(j)): J -> Set): Set
Furthermore, we also know from the Yoneda embedding, that x ~= Hom(x, -) for all x. 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).