Here's a theorem from Leinster's textbook:
He proves it using triangle identities. As I mentioned in a comment to this answer, I suspect that the direct proof (that doesn't appeal to the triangle identities) would be more intuitive. So I attempted to prove this directly (see below), and I was wondering if this proof is correct (modulo the uniqueness part that I couldn't prove). And also I was wondering how to prove uniqueness.
We first prove that given an adjunction between $F$ and $G$ as in (a), there is a natural transformation $\eta$ as in (b). This is just done by defining $\eta$ to be the unit of the given adjunction, and the details are given in Lemma 2.3.5 of Leinster's textbook (triangle identities aren't used in the proof).
Now we need to prove that this correspondence is bijective. That is, if $\eta$ is as described in (b), then there exists a unique adjunction as in (a) with unit $\eta$.
Existence. We know that $\eta_A$ is initial in $(A\implies G)$, i.e., for all $\phi:A\to G(B)$, there is a unique $\phi':F(A)\to B$ such that $\phi=G(\phi')\circ \eta_A$. Define the maps $$\mathscr B(F(A),B)\cong\mathscr A(A,G(B)) \\ \phi' \text{ <–| } \phi\\\psi\mapsto G(\psi)\circ \eta_A$$
Now we need to show that (1) these two maps are inverses of each other, (2) that this bijection is natural in $A$ and $B$, (3) the unit of this adjunction is $\eta$.
(1) First composition: $\phi\mapsto \phi'\mapsto G(\phi ')\circ \eta_A$. Need to show that $\phi=G(\phi ')\circ \eta_A$. But this is exactly the condition mentioned in (b) that we're assuming.
Second composition: $\psi\mapsto G(\psi)\circ \eta_A \mapsto (G(\psi)\circ \eta_A)'$. Need to show that $\psi = (G(\psi)\circ \eta_A)'$. By definition, $(G(\psi)\circ \eta_A)'$ is the unique arrow $F(A)\to B$ with the property that $G(\psi)\circ \eta_A=G((G(\psi)\circ \eta_A)')\circ \eta_A$. But $\psi$ is also an arrow $F(A)\to B$ that makes the same triangle commute. Thus $(G(\psi)\circ \eta_A)'=\psi$.
(2) Naturality in $B$ amounts to the commutativity of this diagram:
and it follows from the fact that $G$ is a functor that the diagram commutes.
Naturality in $A$ amounts to the commutativity of this diagram:
and this follows from the fact that $\eta$ is a natural transformation ($\eta$ being a natural transformation implies that $\eta_A\circ p=GF(p)\circ \eta_{A'}$, and now we just need to compose this with $G(\psi)$ to get the commutativity of the diagram above).
(3) To check that $\eta$ is the unit of the adjunction we defined, we need to check that $1_{F(A)}$ goes to $\eta_A$ under the adjunction map. Indeed, $1_{F(A)}\mapsto G(1_{F(A)})\circ \eta_A=1_{GF(A)}\circ \eta_A=\eta_A$.
This proves existence.
Uniqueness.
I don't know how to approach this. Any ideas? (Again, Leinster gives a proof of this using the triangle identities, but I'd like to avoid using them.)
Best Answer
The suggested approach to uniqueness is the approach you already used on other level, namely let $X:=\{$adjunctions between $F$ and $G\}$ and $Y:=\{$natural transformations $\eta:1_{\mathcal A}\to GF$ such that...$\}$, and specify two maps $\Phi:X\to Y$ and $\Psi:Y\to X$ and verify that they are inverses of each other.
Part of this work is already done: we have $\Phi$ of an adjunction is just its unit, and in the 'existence' part you describe a nice candidate for $\Psi$, and you also have $\Phi(\Psi(\eta))=\eta$.
So, the only missing part is $\Psi(\Phi(\alpha))=\alpha$ where $\alpha$ is a natural bijection with components $\alpha_{A,B}:\mathcal B(FA,B)\to \mathcal A(A,GB)$ determining the adjunction.
Let's name these $\mathcal A^{op}\times\mathcal B\to \mathcal Set$ functors: $$U:=\mathcal B(F-,-),\ \quad\ V:=\mathcal A(-,G-)\,,$$ so that $\alpha:U\to V$ is a natural isomorphism.
Note that if $f:A\to A',\ g:B\to B'$ then $$U(f,g)=\underset{FA'\to B}h\,\mapsto\ \underset{FA\to B'}{g\circ h\circ Ff}\\ V(f,g)=\underset{A'\to GB}h\,\mapsto\ \underset{A\to GB'}{Gg\circ h\circ f} \,. $$
By your definition of $\Psi$, we have $\Psi(\eta)_{A,B}=\underset{FA\to B}g\,\mapsto \ Gg\circ\eta_A$.
Now, if we spell out what the unit specifically is for the adjunction given by $\alpha$, we simply obtain $$\eta_A=\alpha_{A,FA}(1_{FA})\,,$$ then by naturality of $\alpha$ we get for any $g:FA\to B$ $$\Psi(\Phi(\alpha))_{A,B}\,(g)\ = Gg\circ \alpha_{A,FA}(1_{FA})\ = \ V(1_A,g)\big(\alpha_{A,FA}(1_{FA})\big)\ = \\ \ = \alpha_{A,B}\circ U(1_A,g)\,\big(1_{FA}) \ = \ \alpha_{A,B}(g)\,.$$