mathlib3

40fdf72d - feat(category_theory/endofunctor/algebra): Define coalgebras over an endofunctor and prove an equivalence (#14834)

feat(category_theory/endofunctor/algebra): Define coalgebras over an endofunctor and prove an equivalence (#14834) This PR dualises the definition of an algebra over an endofunctor to that of a coalgebra over an endofunctor. Furthermore, it proves that if an endofunctor `F` is left adjoint to an endofunctor `G`, then the category of algebras over `F` is equivalent to the category of coalgebras over `G`. Co-authored-by: jlh <48520973+Jlh18@users.noreply.github.com>