The proof that $u \in F(A)$ is sufficient to define a natural transformation $\alpha : \text{Hom}(A, \cdot) \Rightarrow F(\cdot)$ goes like this:
Let $\alpha_X : g \in \text{Hom}(X, Y) \mapsto F(f)(u)$ where $u:= \alpha_A(\text{id}_A)$. What we're trying to prove is:
$$ (\alpha_Y \circ g)(\xi) = ((Fg)\circ \alpha_X)(\xi) ,$$ forall $\xi \in \text{Hom}(A, X)$. But this is $\Leftarrow$ by (via our definitions and functoriality, and associativity):
$$ \alpha_Y(g\circ \xi) = F(g\circ \xi)(u) = ((Fg) \circ (F\xi))(u) = \\ (Fg)\circ ((F\xi)(u)) = (Fg) \circ \alpha_X(\xi) = ((Fg)\circ \alpha_X)(\xi) $$
Was wondering if that all can be compressed into one or a few diagrams (the implications of equality). Above is what I call a compositional algebraic proof. But I'm doing as much visual as I can in BananaCats (my app), so was just wondering...
Also what's it called when you promote an element of a hom-set to an actual morphism and vise versa? Because the proof above implicitly used that fact in several places, yet we don't have a name for it?
Now here shows some features that my app should have including commutation color highlighting.
What your not seeing is the diagram of category $C$ on the left with $\text{Hom}(A, \cdot)$ and $F(\cdot)$ arrows going to this category diagram (essentially representing functors), the fact that most of the above diagram was drawn merely by seeding $C$ with $f$ and $g$ (as morphisms) and that when the user takes an element of $\text{Hom}(A, X)$ it shows up in $C$ or vise versa.