Commit 2022-03-14 07:05 f8d947c7
View on Github →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.