https://en.wikipedia.org/wiki/Yoneda_lemma#Proof
The part I'm not getting is the last one:
Moreover, any element ${\displaystyle u\in F(A)}$ defines a natural transformation in this way.
So we want to determine a natural transformation by $u \in F(A)$ and the obvious choice is to define $\alpha_X(g) = (Fg)u$ where $u =: \alpha_A(\text{id}_A)$ is defined that way.
To prove naturality we need to show that $(Fg) \alpha_X = \alpha_Y \text{Hom}(A, g)$ or that $F(g)\alpha_X(\xi) = \alpha_Y g (\xi)$ for all $\xi \in \text{Hom}(X, X)$, but we have by our above definitions:
$$ F(g) \alpha_X(\xi) = \alpha_Y \circ g \circ \xi = (F g) \alpha_A(\text{id}_A) $$
I think I messed up somewhere. What is the most concise 1 to 3 line proof using the above not-so-well developed vernacular?
I'm in the process of designing how BananaCats would help the user prove Yoneda, and the diagram on the wiki page is perfect. Now, if I could only understand it, then I could write better software, perhaps.
By the way, I'm on the 3rd rewrite of BananaCats. Drag-and-drop works which has the natural side effect of copy / paste. Undo redo works beautifully and...
the undo/redo stack saves to file! So when you restart your computer (or something) you can go back to what you were working on and still undo old changes! $F$ yeah!
It should be for any $u \in F(A)$ define $\alpha(u)_X(f: A \to X) = (Ff)(u)$ and so for any $g : Z \to Y$ in $C$ we have to prove $\alpha_Y \circ \text{Hom}(A, g) = F(g) \circ \alpha_Z$ on all inputs $\xi \in \text{Hom}(A, Z)$. But the goal equation expands to:
$$ \alpha_Y \circ g \circ \xi = (Fg) \circ \alpha_Z(\xi) = (Fg)\circ(F\xi)(u) = F(g)\circ F(\xi) (u) = \\ F(g\circ \xi) (u) = \alpha_Y \circ(g \circ \xi) = \alpha_Y \circ g \circ \xi $$
Amazing! I love proving Yoneda.