Theorem. Lambek's [math-000H]

The evaluator $j$ of an initial algebra $(F, i, j)$ is an isomorphism.

Proof

Let $F\;i$ be an initial in the $F$ -algebra category, the following diagram commutes for any $C$ -object $a$

Now, replace $a$ with $F\;i$ , we have commute diagram

Then we consider a trivial commute diagram by duplicating the path $F\;i \to i$

Combine two diagrams, then we get another commute diagram

By definition now we know $j \circ m$ is a homomorphism, and since $F\;i$ is an initial, we must have

Therefore, we also have

so $m$ is the inverse of $j$ , proves $j$ is an isomorphism.