add endofunctor.algebra (#12642)
This is the second attempt at the following outdated pull request: https://github.com/leanprover-community/mathlib/pull/12295
The original post:
In this PR I define algebras of endofunctors, make the forgetful functor to the ambient category, and show that initial algebras have isomorphisms as their structure maps. This is mostly taken from `monad.algebra`.
