@EricRogstad Recall that a morphism in the category of F-algebras is a function `m :: a -> b` mapping `f :: f a -> a` to `g :: f b -> b` by obeying the law:
m . f = g . fmap m
In order to show that `Fix :: f (Fix f) -> Fix f` is initial, we need to find for every other algebra `h :: f c -> c` some `m :: Fix f -> c` where the rule above is obeyed...
[EDIT: Formatting, fixing F-algebra morphism law]