Do counit-unit adjunctions have the expected universal properties? Let a unit-counit adjunction between the categories $C$ and $D$ be defined as a pair of functors $F: D\rightarrow C$ and $G: C\rightarrow D$ with natural transformations $\varepsilon : FG \rightarrow 1_C$ and $\eta: 1_D \rightarrow GF$ such that $$G\varepsilon \circ\eta G=1_G$$ and $$\varepsilon F \circ F\eta = 1_F$$ i.e. for all objects $A\in C$, $G(\varepsilon_A)\circ \eta_{G(A)}=1_{G(A)}$ and for all objects $B\in D$, $\varepsilon_{F(B)}\circ F(\eta_B) = 1_{F(B)}$.
How would I prove that a unit-counit adjunction has the following universal properties?


*

*Given $B\in D$, $A\in C$, and $f:B\rightarrow G(A)$, there exists a unique morphism $g: F(B)\rightarrow A$ such that $G(g)\circ\eta_B = f$.

*Given $B\in D$, $A\in C$, and $g: F(B)\rightarrow A$, there exists a unique morphism $f: B\rightarrow G(A)$ such that $\varepsilon_A \circ F(f)=g$.
I can see how to prove (say) property 1 for $B,f\in \textrm{Im} G$, which would be a complete proof iff $G$ was surjective: Let $B=G(B_0)$, $f=G(f_0)$. Then $g=f_0 \circ \varepsilon_{B_0}$ works: $G(g)\circ \eta_B=G(f_0)\circ G(\varepsilon_{B_0}) \circ \eta_{G(B_0)}=G(f_0)\circ 1_{G(B_0)}=f$.
But I can't see how to do this for all $B,f\in D$.
 A: Because the unit-counit definition of an adjunction is purely equational, you should expect that these proofs can be done purely equationally, in the same way that you can prove that inverses in a monoid are unique equationally. Also, the second proof is dual to the first so we just need to do the first. 
By far the hardest part of this proof is finding notation to write it in. It's cleanest to use string diagrams, but here's one way to write it that isn't too bad.
First, $g$ can be taken to be the composite
$$F(B) \xrightarrow{F(f)} FG(A) \xrightarrow{\varepsilon_A} A.$$ 
To verify that this choice works, we compute $G(g) \circ \eta_B$: this is the composite
$$B \xrightarrow{\eta_B} GF(B) \xrightarrow{GF(f)} GFG(A) \xrightarrow{G(\varepsilon_A)} G(A).$$
By the naturality of $\eta_B$ (this is much easier to notice with string diagrams), this can be rewritten
$$B \xrightarrow{f} G(A) \xrightarrow{\eta_{G(A)}} GFG(A) \xrightarrow{G(\varepsilon_A)} G(A)$$
and this is equal to $f$ by the first zigzag identity.
This proves that $g$ exists. To prove that it is unique, we'll show that if $f$ is equal to 
$$B \xrightarrow{\eta_B} GF(B) \xrightarrow{G(g)} G(A)$$
then $g$ must be the above composite. To verify that this works, we compute $\varepsilon_A \circ F(f)$: this is the composite
$$F(B) \xrightarrow{F(\eta_B)} FGF(B) \xrightarrow{FG(g)} FG(A) \xrightarrow{\varepsilon_A} A.$$
By the naturality of $\varepsilon_A$, this can be rewritten
$$F(B) \xrightarrow{F(\eta_B)} FGF(B) \xrightarrow{\varepsilon_{F(B)}} F(B) \xrightarrow{g} A$$
and this is equal to $g$ by the second zigzag identity. 
You can interpret this proof as showing that the unit and counit can be used to write down an explicit (natural) bijection $\text{Hom}(F(B), A) \cong \text{Hom}(B, G(A))$; the unit gives the map in one direction, the counit gives the map in the other direction, and the fact that they're mutually inverse is equivalent to the zigzag identities. 
