# Initial F-algebra and its isomorphic arrow proof

A very stupid question from a programmer here.

There is a theorem in Pierce's "Basic category theory for computer scientists" that sounds as follows:

Let $K$ be a category, and $F$ be an endofunctor on this category. If $F$-Algebra ($A$, $a:F(A)\rightarrow A$) is initial in $F$-$Alg$ category, then $a$ is isomorphism in $K$.

Now, I can easily show that there is an arrow $h:A\rightarrow F(A)$, which is a unique $F$-homomorphism $(A, a)\rightarrow (F(A), F(a))$, and that $a\circ h = id_A$, because $a\circ h$ is a $F$-homomorphism $(A, a)\rightarrow (A, a)$, which can only be $id_A$ due to initiality of $(A, a)$.

But when it comes to showing that $h\circ a = id_{F(A)}$, I get somewhat stuck. It's obvious that I'm missing something simple, but could anybody help with finding what exactly it would be?

-

From $a \circ h = id_A$ you can deduce from the functoriality of $F$ that $F(a) \circ F(h) = id_{F(a)}$. But by definition of $h$ you have a commutative square: $$\begin{array}{ccc} F(A) & \xrightarrow{a} & A \\ \downarrow F(h) & & \downarrow h \\ F(F(A)) & \xrightarrow{F(a)} & F(A) \end{array}$$ Therefore $h \circ a = F(a) \circ F(h) = id_{F(A)}$.