A Universe of Sorts

Let $J$ be small, $C$ locally small.
Let $F: J \to C$ be a diagram. Let $y : C \to [C^{op}, Set]$ be the contravariant yoneda defined by $y(c) \equiv Hom(-, c)$ .
Consider $y(\lim F) : C^{op} \to Set$ . Is this equal to $\lim (y \circ F : J \to [C^{op}, Set) : C^{op} \to Set$ ?
We know that limits in functor categories are computed pointwise. So let's start with $\lim (y \circ F) : C^{op} \to Set$ . Let's Evaluate at some $e \in C^{op}$ .
That gives us $(\lim (y \circ F))(e) = \lim (ev_e \circ y \circ F : J \to Set) : Set$ .
Writing the above out, we get $\lim (ev_e \circ y \circ F) = \lim(\lambda j. (y(F(j))(e))$ .
Plugging in the definition of $y$ , we ge $\lim( \lambda j. Hom(-, F(j))(e))$ .
Simplifying, we get $\lim (\lambda j. Hom(e, F(j))$ .
We know from a previous theorem that $\lim Hom(e, F(-)) = = Hom(e, \lim F)$
Thus, we get $\lim(\lambda j. Hom(e, F(j)) = Hom(e, \lim F)$ .
So we get $(\lim (y \circ F))(e) = Hom(e, \lim F)$ .
In general, we get $\lim (y \circ F) = Hom(-, \lim F)$ , which is the same as $y \circ \lim F$ .
So we find that $\lim (y \circ F) = y \circ \lim F$ , thereby proving that yoneda preserves limits.

§ Yoneda Preserves Limits