I'm confused in the way Barr and Wells proof the uniqueness of adjoints. Once they prove that using Yoneda lemma the two candidates $F,F'$ to be adjoint to some functor $U$ satisfy $F A \cong F' A$ for any $A$ they conclude by saying that the naturality of the isomorphism is a consequence of the following theorem:
Let $\mathcal{A},\mathcal{B}$ be categories and $U: \mathcal{B} \to \mathcal{A}$ be a functor. Suppose for each object $A$ of $\mathcal{A}$ there is an object $FA$ of $\mathcal{B}$ such that $Hom(FA, \cdot)$ is naturally equivalent to $Hom(A,U \cdot)$ as a functor from $\mathcal{B}$ to $Set$. Then the definition of $F$ on objects can be extended to arrows in such a way that $F$ becomes a functor and is left adjoint to $U$.
I'm assuming naturally equivalent means naturally isomorphic.
Question
Is the following proof correct?
Proof
Let $f:A \to A'$ be an arrow in $\mathcal{A}^{op}$ and denote the $n_A: Hom(FA, \cdot) \stackrel{\cong}{\to} Hom(A,U \cdot)$. Then we have the diagram:
If an arrow $Hom(FA',B) \to Hom(FA,B)$ makes the diagram commute it is necessarily: $$\phi(f,B) = n_A \circ Hom(f,UB) \circ n_{A'}^{-1}$$ But actually, $\phi(f,\cdot): Hom(FA',\cdot) \to Hom(FA,\cdot)$ is a natural transformation in $B$ since $n_A, n_{A'}$ and $Hom(f,U \cdot)$ are natural in $B$. By the Yoneda lemma, there exists a unique $B \in Hom(F A', F A)$ such that $Y(B) = Hom(B, \cdot) = \phi(f, \cdot)$. We define $F f = B: FA \to FA'$ as a morphism in $\mathcal{C}^{op}$.
We check that $F$ defined in this way is a functor.
$\phi(id_A, \cdot) = n_A \circ Hom(id_A,\cdot) \circ n_{A}^{-1} = n_A \circ n_A^{-1} = id$
$ \phi(f , \cdot) \circ \phi(g, \cdot) = n_A \circ Hom(f, \cdot) \circ n_{A'}^{-1} \circ n_{A'} \circ Hom(g,\cdot) \circ n_{A''}^{-1} = n_A \circ Hom(f,\cdot) \circ Hom(g,\cdot) \circ n_{A''}^{-1} = n_A \circ Hom(f \circ g, \cdot) \circ n_{A''}^{-1} = \phi(f \circ g, \cdot) $
It remains to check that $F$ is left adjoint to $U$. However, the above diagram states precisely the naturality in $A$ of the isomorphism while by hypothesis we have the naturality in $B$. These two lead to the conclusion that $F$ built in this way is left adjoint to $U$.
Question
My conclusion is that up to the choice of $n$ above, $F$ is uniquely determined. So this is indeed a proof of the uniqueness of adjoints up to isomorphism. Is that right?