[proofplan] The proof constructs the inverse map explicitly. A natural transformation $\eta: \operatorname{Hom}_{\mathcal{C}}(A,-) \to F$ is determined by the single element $\eta_A(\operatorname{id}_A) \in F(A)$, because naturality transports this element along every morphism $f: A \to X$. Conversely, each element $a \in F(A)$ defines a natural transformation by sending $f: A \to X$ to $F(f)(a)$. We then verify that these constructions are inverse and check the two naturality assertions. [/proofplan] [step:Define evaluation at the identity morphism] Since $\mathcal{C}$ is locally small, each collection $\operatorname{Hom}_{\mathcal{C}}(A,X)$ is a set, so $\operatorname{Hom}_{\mathcal{C}}(A,-): \mathcal{C} \to \mathbf{Set}$ is a well-defined functor. Define \begin{align*} \Phi_{A,F}: \operatorname{Nat}(\operatorname{Hom}_{\mathcal{C}}(A,-),F) &\to F(A) \\ \eta &\mapsto \eta_A(\operatorname{id}_A). \end{align*} Here $\eta_A: \operatorname{Hom}_{\mathcal{C}}(A,A) \to F(A)$ is the component of the natural transformation $\eta$ at $A$, and $\operatorname{id}_A \in \operatorname{Hom}_{\mathcal{C}}(A,A)$ is the identity morphism of $A$. [/step] [step:Construct a natural transformation from an element of $F(A)$] Let $a \in F(A)$. For every object $X$ of $\mathcal{C}$, define a function \begin{align*} \Psi_{A,F}(a)_X: \operatorname{Hom}_{\mathcal{C}}(A,X) &\to F(X) \\ f &\mapsto F(f)(a). \end{align*} We claim that the family $\Psi_{A,F}(a) = (\Psi_{A,F}(a)_X)_X$ is a natural transformation \begin{align*} \Psi_{A,F}(a): \operatorname{Hom}_{\mathcal{C}}(A,-) \to F. \end{align*} Let $g: X \to Y$ be a morphism in $\mathcal{C}$. We must prove that the square \begin{align*} \operatorname{Hom}_{\mathcal{C}}(A,X) \xrightarrow{\Psi_{A,F}(a)_X} F(X) \end{align*} and \begin{align*} \operatorname{Hom}_{\mathcal{C}}(A,Y) \xrightarrow{\Psi_{A,F}(a)_Y} F(Y) \end{align*} commutes with the vertical maps $\operatorname{Hom}_{\mathcal{C}}(A,g)$ and $F(g)$. Thus let $f \in \operatorname{Hom}_{\mathcal{C}}(A,X)$. By the definition of $\operatorname{Hom}_{\mathcal{C}}(A,g)$ and by functoriality of $F$, \begin{align*} \Psi_{A,F}(a)_Y(\operatorname{Hom}_{\mathcal{C}}(A,g)(f)) &= \Psi_{A,F}(a)_Y(g \circ f) \\ &= F(g \circ f)(a) \\ &= (F(g) \circ F(f))(a) \\ &= F(g)(\Psi_{A,F}(a)_X(f)). \end{align*} Therefore $\Psi_{A,F}(a)$ is natural. [guided] Let $a \in F(A)$. The intended inverse to evaluation should turn $a$ into a natural transformation out of the representable functor. For an object $X$, an element of $\operatorname{Hom}_{\mathcal{C}}(A,X)$ is a morphism $f: A \to X$. Since $F$ is covariant, $F$ sends $f$ to a function \begin{align*} F(f): F(A) \to F(X). \end{align*} Therefore $F(f)(a)$ is an element of $F(X)$. This gives the component \begin{align*} \Psi_{A,F}(a)_X: \operatorname{Hom}_{\mathcal{C}}(A,X) &\to F(X) \\ f &\mapsto F(f)(a). \end{align*} We now verify naturality. Let $g: X \to Y$ be a morphism in $\mathcal{C}$, and let $f \in \operatorname{Hom}_{\mathcal{C}}(A,X)$. The representable functor sends $g$ to the function \begin{align*} \operatorname{Hom}_{\mathcal{C}}(A,g): \operatorname{Hom}_{\mathcal{C}}(A,X) &\to \operatorname{Hom}_{\mathcal{C}}(A,Y) \\ f &\mapsto g \circ f. \end{align*} Thus the lower-left route in the naturality square gives \begin{align*} \Psi_{A,F}(a)_Y(\operatorname{Hom}_{\mathcal{C}}(A,g)(f)) &= \Psi_{A,F}(a)_Y(g \circ f) \\ &= F(g \circ f)(a). \end{align*} Since $F$ is a functor, it preserves composition, so $F(g \circ f) = F(g) \circ F(f)$. Hence \begin{align*} F(g \circ f)(a) &= (F(g) \circ F(f))(a) \\ &= F(g)(F(f)(a)) \\ &= F(g)(\Psi_{A,F}(a)_X(f)). \end{align*} This is exactly the equality required for the naturality square to commute. Therefore $\Psi_{A,F}(a): \operatorname{Hom}_{\mathcal{C}}(A,-) \to F$ is a natural transformation. [/guided] [/step] [step:Show that the two constructions are inverse] First let $a \in F(A)$. By the definition of $\Psi_{A,F}(a)_A$ and by preservation of identities by $F$, \begin{align*} (\Phi_{A,F} \circ \Psi_{A,F})(a) &= \Phi_{A,F}(\Psi_{A,F}(a)) \\ &= \Psi_{A,F}(a)_A(\operatorname{id}_A) \\ &= F(\operatorname{id}_A)(a) \\ &= \operatorname{id}_{F(A)}(a) \\ &= a. \end{align*} Thus $\Phi_{A,F} \circ \Psi_{A,F} = \operatorname{id}_{F(A)}$. Conversely, let \begin{align*} \eta: \operatorname{Hom}_{\mathcal{C}}(A,-) \to F \end{align*} be a natural transformation. We prove that $\Psi_{A,F}(\Phi_{A,F}(\eta)) = \eta$ componentwise. Let $X$ be an object of $\mathcal{C}$ and let $f \in \operatorname{Hom}_{\mathcal{C}}(A,X)$. Naturality of $\eta$ with respect to the morphism $f: A \to X$ gives \begin{align*} F(f) \circ \eta_A = \eta_X \circ \operatorname{Hom}_{\mathcal{C}}(A,f). \end{align*} Evaluating both sides at $\operatorname{id}_A \in \operatorname{Hom}_{\mathcal{C}}(A,A)$ gives \begin{align*} F(f)(\eta_A(\operatorname{id}_A)) &= \eta_X(\operatorname{Hom}_{\mathcal{C}}(A,f)(\operatorname{id}_A)) \\ &= \eta_X(f \circ \operatorname{id}_A) \\ &= \eta_X(f). \end{align*} Using the definitions of $\Phi_{A,F}$ and $\Psi_{A,F}$, this says \begin{align*} \Psi_{A,F}(\Phi_{A,F}(\eta))_X(f) &= F(f)(\eta_A(\operatorname{id}_A)) \\ &= \eta_X(f). \end{align*} Since $X$ and $f$ were arbitrary, $\Psi_{A,F}(\Phi_{A,F}(\eta)) = \eta$. Therefore $\Phi_{A,F}$ is a bijection with inverse $\Psi_{A,F}$. [guided] We must show that evaluation at $\operatorname{id}_A$ loses no information. First take $a \in F(A)$. Applying $\Psi_{A,F}$ gives the natural transformation whose component at $A$ is \begin{align*} \Psi_{A,F}(a)_A: \operatorname{Hom}_{\mathcal{C}}(A,A) &\to F(A) \\ h &\mapsto F(h)(a). \end{align*} Evaluating this component at $\operatorname{id}_A$ gives \begin{align*} (\Phi_{A,F} \circ \Psi_{A,F})(a) &= \Psi_{A,F}(a)_A(\operatorname{id}_A) \\ &= F(\operatorname{id}_A)(a). \end{align*} Because $F$ is a functor, it preserves identity morphisms, so $F(\operatorname{id}_A)=\operatorname{id}_{F(A)}$. Hence \begin{align*} (\Phi_{A,F} \circ \Psi_{A,F})(a) &= \operatorname{id}_{F(A)}(a) \\ &= a. \end{align*} Now take a natural transformation \begin{align*} \eta: \operatorname{Hom}_{\mathcal{C}}(A,-) \to F. \end{align*} We need to recover every component $\eta_X$ from the single element $\eta_A(\operatorname{id}_A)$. Let $X$ be an object of $\mathcal{C}$ and let $f: A \to X$ be a morphism. The key point is that $f$ is obtained from $\operatorname{id}_A$ by applying the representable functor to $f$: \begin{align*} \operatorname{Hom}_{\mathcal{C}}(A,f)(\operatorname{id}_A) &= f \circ \operatorname{id}_A \\ &= f. \end{align*} Naturality of $\eta$ with respect to $f: A \to X$ says that \begin{align*} F(f) \circ \eta_A = \eta_X \circ \operatorname{Hom}_{\mathcal{C}}(A,f). \end{align*} Evaluating this equality of functions at $\operatorname{id}_A$ gives \begin{align*} F(f)(\eta_A(\operatorname{id}_A)) &= \eta_X(\operatorname{Hom}_{\mathcal{C}}(A,f)(\operatorname{id}_A)) \\ &= \eta_X(f). \end{align*} The left-hand side is exactly the value assigned by $\Psi_{A,F}(\Phi_{A,F}(\eta))_X$ to $f$, because $\Phi_{A,F}(\eta)=\eta_A(\operatorname{id}_A)$. Thus \begin{align*} \Psi_{A,F}(\Phi_{A,F}(\eta))_X(f) = \eta_X(f). \end{align*} Since this holds for every object $X$ and every morphism $f: A \to X$, the two natural transformations are equal. Therefore $\Phi_{A,F}$ and $\Psi_{A,F}$ are inverse bijections. [/guided] [/step] [step:Verify naturality in the functor $F$] Let \begin{align*} \alpha: F \to G \end{align*} be a natural transformation between functors $F,G: \mathcal{C} \to \mathbf{Set}$. We prove that the bijections commute with postcomposition by $\alpha$. Let \begin{align*} \eta: \operatorname{Hom}_{\mathcal{C}}(A,-) \to F \end{align*} be a natural transformation. Then $\alpha \circ \eta: \operatorname{Hom}_{\mathcal{C}}(A,-) \to G$ is the natural transformation with component $(\alpha \circ \eta)_X = \alpha_X \circ \eta_X$ at each object $X$. Therefore \begin{align*} \Phi_{A,G}(\alpha \circ \eta) &= (\alpha_A \circ \eta_A)(\operatorname{id}_A) \\ &= \alpha_A(\eta_A(\operatorname{id}_A)) \\ &= \alpha_A(\Phi_{A,F}(\eta)). \end{align*} Thus the square expressing naturality in $F$ commutes. [/step] [step:Verify naturality in the representing object $A$] Let $B$ be an object of $\mathcal{C}$, and let $u: B \to A$ be a morphism in $\mathcal{C}$. Define the natural transformation \begin{align*} H_u: \operatorname{Hom}_{\mathcal{C}}(A,-) \to \operatorname{Hom}_{\mathcal{C}}(B,-) \end{align*} by the component functions \begin{align*} (H_u)_X: \operatorname{Hom}_{\mathcal{C}}(A,X) &\to \operatorname{Hom}_{\mathcal{C}}(B,X) \\ f &\mapsto f \circ u \end{align*} for each object $X$ of $\mathcal{C}$. Let \begin{align*} \eta: \operatorname{Hom}_{\mathcal{C}}(B,-) \to F \end{align*} be a natural transformation. We compare $\Phi_{A,F}(\eta \circ H_u)$ with $F(u)(\Phi_{B,F}(\eta))$. By definition of composition of natural transformations, \begin{align*} \Phi_{A,F}(\eta \circ H_u) &= (\eta_A \circ (H_u)_A)(\operatorname{id}_A) \\ &= \eta_A(\operatorname{id}_A \circ u) \\ &= \eta_A(u). \end{align*} Naturality of $\eta$ with respect to $u: B \to A$ gives \begin{align*} F(u) \circ \eta_B = \eta_A \circ \operatorname{Hom}_{\mathcal{C}}(B,u). \end{align*} Evaluating at $\operatorname{id}_B \in \operatorname{Hom}_{\mathcal{C}}(B,B)$ yields \begin{align*} F(u)(\eta_B(\operatorname{id}_B)) &= \eta_A(\operatorname{Hom}_{\mathcal{C}}(B,u)(\operatorname{id}_B)) \\ &= \eta_A(u \circ \operatorname{id}_B) \\ &= \eta_A(u). \end{align*} Therefore \begin{align*} \Phi_{A,F}(\eta \circ H_u) = F(u)(\Phi_{B,F}(\eta)). \end{align*} This is precisely the naturality condition in the representing object. Combining this with the previous steps proves the Yoneda bijection and its naturality in both variables. [/step]