Commit 2024-07-04 14:02 1b306ae5

feat(CategoryTheory): Special equalizers associated to a comonad (#14171) Given a comonad, shows that any coalgebra is an equalizer (in the category of coalgebras) of cofree coalgebras, and shows this equalizer is coreflexive. Also constructs the Beck fork in the category of coalgebras, and shows the fork is coreflexive as well as a split equalizer (in particular, an equalizer). This dualises everything in Mathlib.CategoryTheory.Monad.Coequalizer. This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024.