§ Yoneda preserves limits

• 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.