I'm trying to prove that that the naturality squares commute for the natural transformation $\epsilon F$ defined by $(\epsilon F)_A=\epsilon_{F(A)}:FGF(A)\to F(A)$ where $\epsilon$ is the counit of adjunction between $F$ and $G$ ($F$ on the left and $G$ on the right). So I need to prove that for any arrow $f:A\to A'$ in the domain category of $F$, the following square commutes
The only idea I had is to use the commutativity of the naturality squares for $\epsilon_X$:
But I don't see how to do it. Applying $F$ to this diagram wouldn't make any sense. I could consider a diagram with vertical arrows $GF(X)\to X$ with $X=A,A'$ and apply $F$ but that diagram doesn't make sense to me, why would it be commutative (the naturality squares for the unit of adjunction $\eta$ should go in the opposite direction)?
How to proceed?
Your first naturality square is just your second square applied at the morphism $\alpha = F(f): F(A) \rightarrow F(A')$.
That is, the naturality square for $\epsilon$ commutes for every morphism $\alpha$ in the source category of $G$. $F(f)$ is one specific morphism in the source category of $G$, so we can substitute it in as a possible $\alpha$ and get a commuting square.
This works for all $f:A \rightarrow A'$, so we get all the commuting squares we need for a natural transformation $FGF \Rightarrow F$.