Equivalent conditions for equivalence of categories (Proposition 7.26 in Awodey) I'm trying to understand the proof of the following proposition in Steve Awodey's "Category Theory".
Let $\mathbf{C}, \mathbf{D}$ be categories and let $F: \mathbf{C} \to \mathbf{D}$ be a functor. The following conditions are equivalent:
(1) $F$ is part of an equivalence of categories between $\mathbf{C}$ and $\mathbf{D}$.
(2) $F$ is full and faithful and ``essentially surjective'' on objects:
\begin{equation*}
\forall D \in \mathbf{D}. \, \exists C \in \mathbf{C}. \, FC \cong D.
\end{equation*}

What I don't quite understand is the proof of (2) $\Longrightarrow$ (1). His proof for this is as follows:
We need to define $E: \mathbf{D} \to \mathbf{C}$ and natural transformations
\begin{align*}
\alpha: 1_C \xrightarrow{\sim} E \circ F\\
\beta: 1_D \xrightarrow{\sim} F \circ E
\end{align*}
Since $F$ is essentially surjective, for each $D \in \mathbf{D}_0$, we can choose some $E(D) \in \mathbf{C}_0$ along with some $\beta_D: D \xrightarrow{\sim} FE(D)$. That gives $E$ on objects and the proposed components of $\beta: 1_{\mathbf{D}} \to FE$. Given $h: D \to D'$ in $\mathbf{D}$, consider
$$
\beta_{D'} \circ h = (\beta_{D'} \circ h \circ \beta_{D}^{-1}) \circ \beta_D
$$
Since $F: \mathbf{C} \to \mathbf{D}$ is full and faithful, there is a unique arrow
$$
E(h): E(D) \to E(D')
$$
with $FE(h) = \beta_{D'} \circ h \circ \beta_{D}^{-1}$. It is easy to see that then $E: \mathbf{D} \to \mathbf{C}$ is a functor and $\beta: 1_{\mathbf{D}} \xrightarrow{\sim} FE$ is clearly a natural isomorphism.
To find $\alpha: 1_{\mathbf{C}} \to EF$, apply $F$ to any $C$ and consider $\beta_{FC}: F(C) \to FEF(C)$. Since $F$ is full and faithful, the preimage of $\beta_{FC}$ is an isomorphism,
$$
\alpha_C = F^{-1}(\beta_{FC}): C \xrightarrow{\sim} EF(C)
$$
which is easily seen to be natural, since $\beta$ is.

Why does this construction make $E$ a functor?
I guess we just choose $E(1_D) = 1_{ED}$, but how do we know that $E(f \circ g) = E(f) \circ E(g)$?
And why do we know that $\beta$ is a natural isomorphism?
I get that we choose $\beta_D$ to be an isomorphism, but why is $\beta$ natural?
 A: Let me actually give a full answer, as this is an important point in category theory.

Proof of the fact that $E$ is a functor:
For every arrow $h:D\rightarrow D^{\prime}$ in $\mathbf{D}$, you have defined
$E\left(  h\right)  $ as the unique arrow $h^{\prime}:E\left(  D\right)
\rightarrow E\left(  D^{\prime}\right)  $ with $F\left(  h^{\prime}\right)
=\beta_{D^{\prime}}\circ h\circ\beta_{D}^{-1}$. Therefore,
(1) the arrow $E\left(  h\right)  $ satisfies $F\left(  E\left(  h\right)
\right)  =\beta_{D^{\prime}}\circ h\circ\beta_{D}^{-1}$,
and furthermore (by the "uniqueness" part
of the preceding sentence)
(2) every arrow $h^{\prime}:E\left(  D\right)  \rightarrow E\left(
D^{\prime}\right)  $ satisfying $F\left(  h^{\prime}\right)  =\beta
_{D^{\prime}}\circ h\circ\beta_{D}^{-1}$ must satisfy $h^{\prime}=E\left(
h\right)  $.
Let us now show that
(3) $E\left(  1_{D}\right)  =1_{E\left(  D\right)  }$ for every object $D$
of $\mathbf{D}$.
In fact, let $D$ be an object of $\mathbf{D}$. Then, $1_{E\left(  D\right)  }$
is an arrow $E\left(  D\right)  \rightarrow E\left(  D\right)  $. Since $F$ is
a functor, we have $F\left(  1_{E\left(  D\right)  }\right)  =1_{F\left(
E\left(  D\right)  \right)  }=\beta_{D}\circ1_{D}\circ\beta_{D}^{-1}$ (since
$\beta_{D}\circ1_{D}\circ\beta_{D}^{-1}=\beta_{D}\circ\beta_{D}^{-1}
=1_{F\left(  E\left(  D\right)  \right)  }$). Therefore, (2) (applied to
$D^{\prime}=D$, $h=1_{D}$ and $h^{\prime}=1_{E\left(  D\right)  }$) satisfies
$1_{E\left(  D\right)  }=E\left(  1_{D}\right)  $. This proves (3).
(Note that your argument that "we just choose $E\left(
1_{D}\right)  =1_{ED}$" is somewhat imprecise: We are not
choosing everything, since $E\left(  h\right)  $ is defined as the
unique arrow $h^{\prime}:E\left(  D\right)  \rightarrow E\left(
D^{\prime}\right)  $ with $F\left(  h^{\prime}\right)  =\beta_{D^{\prime}
}\circ h\circ\beta_{D}^{-1}$. Things that are unique are not "chosen".
But other than this, your argument is the same as mine.)
Now, let us show that
(4) $E\left(  f\circ g\right)  =E\left(  f\right)  \circ E\left(
g\right)  $ for any two arrows $f:D^{\prime}\rightarrow D^{\prime\prime}$ and
$g:D\rightarrow D^{\prime}$ in $\mathbf{D}$.
Indeed, let $f:D^{\prime}\rightarrow D^{\prime\prime}$ and $g:D\rightarrow
D^{\prime}$ be two arrows in $\mathbf{D}$. Since $F$ is a functor, we have
$F\left(  E\left(  f\right)  \circ E\left(  g\right)  \right)
=\underbrace{F\left(  E\left(  f\right)  \right)  }_{\substack{=\beta
_{D^{\prime\prime}}\circ f\circ\beta_{D^{\prime}}^{-1}\\\text{(by
\textbf{(1)}, applied to }D^{\prime}\text{, }D^{\prime\prime}\text{ and
}f\\\text{instead of }D\text{, }D^{\prime}\text{ and }h\text{)}}
}\circ\underbrace{F\left(  E\left(  g\right)  \right)  }_{\substack{=\beta
_{D^{\prime}}\circ g\circ\beta_{D}\\\text{(by \textbf{(1)}, applied to
}h=g\text{)}}}$
$=\beta_{D^{\prime\prime}}\circ f\circ\underbrace{\beta_{D^{\prime}}^{-1}
\circ\beta_{D^{\prime}}}_{=1_{D^{\prime}}}\circ g\circ\beta_{D}=\beta
_{D^{\prime\prime}}\circ f\circ g\circ\beta_{D}$.
Thus, (2) (applied to $D^{\prime\prime}$, $f\circ g$ and $E\left(
f\right)  \circ E\left(  g\right)  $ instead of $D^{\prime}$, $h$ and
$h^{\prime}$) yields $E\left(  f\right)  \circ E\left(  g\right)  =E\left(
f\circ g\right)  $.
Thus, (4) is proven. Combined with (3), this shows that $E$ is a
functor $\mathbf{D}\rightarrow\mathbf{C}$.
(This is a typical example of how to get mileage out of uniqueness statements.
The general intuition is that uniqueness forces things to fit together.)

Proof that $\beta$ is a natural isomorphism:
We shall first show that $\beta$ is a natural transformation. Indeed, in order
to prove this, it is enough to check that for every arrow $h:D\rightarrow
D^{\prime}$ in $\mathbf{D}$, we have
(5) $F\left(  E\left(  h\right)  \right)  \circ\beta_{D}=\beta_{D^{\prime
}}\circ h$.
(This equality (5) is usually written as a commutative diagram, but I
don't know a good way to draw commutative diagrams on math.stackexchange.
xymatrix support anyone?)
But (5) immediately follows from (1): Namely, (1) yields
$F\left(  E\left(  h\right)  \right)  \circ\beta_{D}=\beta_{D^{\prime}}\circ
h\circ\underbrace{\beta_{D}^{-1}\circ\beta_{D}}_{=1_{D}}=\beta_{D^{\prime}
}\circ h$.
Thus, (5) is proven, and it follows that $\beta$ is a natural
transformation. Since $\beta_{D}$ is an isomorphism for every $D\in\mathbf{D}
$, this shows that $\beta$ is a natural isomorphism.

Proof that $\alpha$ is a natural isomorphism:
You did not ask for this proof, but it is harder than the other two things
I've explained, so let me explain it too. There is no such thing as a functor
$F^{-1}:\mathbf{D}\rightarrow\mathbf{C}$, but we can nevertheless write
$F^{-1}\left(  h\right)  $ whenever $C$ and $C^{\prime}$ are two objects of
$\mathbf{C}$ and $h$ is an arrow $F\left(  C\right)  \rightarrow F\left(
C^{\prime}\right)  $ in $\mathbf{D}$. The reason for this is that the functor
$F$ is fully faithful, and thus every arrow $h:F\left(  C\right)  \rightarrow
F\left(  C^{\prime}\right)  $ in $\mathbf{D}$ can be uniquely written in the
form $h=F\left(  h^{\prime}\right)  $ for an arrow $h^{\prime}:C\rightarrow
C^{\prime}$ in $\mathbf{C}$. This latter arrow $h^{\prime}$ is what is denoted
by $F^{-1}\left(  h\right)  $.
Now, the uniqueness again forces things to "fit together". Namely, we have
(6) $F^{-1}\left(  1_{F\left(  C\right)  }\right)  =1_{C}$ for every
object $C$ of $\mathbf{C}$,
and we have
(7) $F^{-1}\left(  f\circ g\right)  =F^{-1}\left(  f\right)  \circ
F^{-1}\left(  g\right)  $
whenever $C$, $C^{\prime}$ and $C^{\prime\prime}$ are three objects of
$\mathbf{C}$ and $f:F\left(  C\right)  \rightarrow F\left(  C^{\prime}\right)
$ and $g:F\left(  C^{\prime}\right)  \rightarrow F\left(  C^{\prime\prime
}\right)  $ are two arrows in $\mathbf{D}$. This can be proven by exploiting
the uniqueness, similarly to how we proved (1) and (3). Actually, this
does make $F^{-1}$ into a functor, but not in the obvious way; instead, if we
define $\mathbf{D}^{\prime}$ to be the category whose objects are the objects
of $\mathbf{C}$ but whose Hom-sets are defined by $\mathbf{D}^{\prime}\left(
C,C^{\prime}\right)  =\mathbf{D}\left(  F\left(  C\right)  ,F\left(
C^{\prime}\right)  \right)  $, then $F^{-1}$ is a functor (actually an
isomorphism of categories) from $\mathbf{D}^{\prime}$ to $\mathbf{D}$.
Caution: This functor acts as the identity on objects, but sends any morphism
$h$ in $\mathbf{D}^{\prime}$ to $F^{-1}\left(  h\right)  $.
Anyway, this functor $F^{-1}$ (or, if you will, just the equalities (6)
and (7)) is what is needed to prove that $\alpha_{C}$ is an isomorphism
for every $C\in\mathbf{C}$. Namely, if $C\in\mathbf{C}$, then (using the fact
that $\beta_{F\left(  C\right)  }$ is invertible) we have
$1_{C}=F^{-1}\left(  \underbrace{1_{F\left(  C\right)  }}_{=\beta_{F\left(
C\right)  }\circ\beta_{F\left(  C\right)  }^{-1}}\right)  $ (by (6))
$=F^{-1}\left(  \beta_{F\left(  C\right)  }\circ\beta_{F\left(  C\right)
}^{-1}\right)  =\underbrace{F^{-1}\left(  \beta_{F\left(  C\right)  }\right)
}_{=\alpha_{C}}\circ F^{-1}\left(  \beta_{F\left(  C\right)  }^{-1}\right)  $
(by (7))
$=\alpha_{C}\circ F^{-1}\left(  \beta_{F\left(  C\right)  }^{-1}\right)  $
and similarly $1_{E\left(  F\left(  C\right)  \right)  }=F^{-1}\left(
\beta_{F\left(  C\right)  }^{-1}\right)  \circ\alpha_{C}$. Hence, $\alpha_{C}$
is invertible, i.e., an isomorphism.
Now, we want to show that $\alpha$ is a natural isomorphism. Since we already
know that $\alpha_{C}$ is an isomorphism for every $C\in\mathbf{C}$, it only
remains to prove that $\alpha$ is a natural transformation. In other words, we
need to show that every two objects $C$ and $C^{\prime}$ of $\mathbf{C}$ and
every arrow $h:C\rightarrow C^{\prime}$ satisfy
(8) $\alpha_{C^{\prime}}\circ h=\left(  EF\right)  \left(  h\right)
\circ\alpha_{C}$.
So let $C$ and $C^{\prime}$ be two objects of $\mathbf{C}$, and let
$h:C\rightarrow C^{\prime}$ be any arrow. The definition of $\alpha_{C}$
yields $\alpha_{C}=F^{-1}\left(  \beta_{F\left(  C\right)  }\right)  $, so
that $F\left(  \alpha_{C}\right)  =\beta_{F\left(  C\right)  }$ and similarly
$F\left(  \alpha_{C^{\prime}}\right)  =\beta_{F\left(  C^{\prime}\right)  }$.
Now, $F$ is a functor, so that
$F\left(  \alpha_{C^{\prime}}\circ h\right)  =\underbrace{F\left(
\alpha_{C^{\prime}}\right)  }_{=\beta_{F\left(  C^{\prime}\right)  }}\circ
F\left(  h\right)  =\beta_{F\left(  C^{\prime}\right)  }\circ F\left(
h\right)  $.
Compared with
$F\left(  \left(  EF\right)  \left(  h\right)  \circ\alpha_{C}\right)
=\underbrace{F\left(  \left(  EF\right)  \left(  h\right)  \right)
}_{\substack{=F\left(  E\left(  F\left(  h\right)  \right)  \right)
\\=\beta_{F\left(  C^{\prime}\right)  }\circ F\left(  h\right)  \circ
\beta_{F\left(  C\right)  }^{-1}\\\text{(by \textbf{(1)}, applied
to}\\F\left(  C\right)  \text{, }F\left(  C^{\prime}\right)  \text{ and
}F\left(  h\right)  \\\text{instead of }D\text{, }D^{\prime}\text{ and
}h\text{)}}}\circ\underbrace{F\left(  \alpha_{C}\right)  }_{=\beta_{F\left(
c\right)  }}$ (since $F$ is a functor)
$=\beta_{F\left(  C^{\prime}\right)  }\circ F\left(  h\right)  \circ
\underbrace{\beta_{F\left(  C\right)  }^{-1}\circ\beta_{F\left(  C\right)  }
}_{=1_{F\left(  C\right)  }}=\beta_{F\left(  C^{\prime}\right)  }\circ
F\left(  h\right)  $,
this yields $F\left(  \alpha_{C^{\prime}}\circ h\right)  =F\left(  \left(
EF\right)  \left(  h\right)  \circ\alpha_{C}\right)  $. Since $F$ is faithful,
this yields $\alpha_{C^{\prime}}\circ h=\left(  EF\right)  \left(  h\right)
\circ\alpha_{C}$. Thus, (8) is proven. So $\alpha$ is a natural isomorphism.
