Monad algebra forgetful functor creates split coequalizers
ID: monad-algebra-forgetful-functor-creates-split-coequalizers
For algebra maps whose underlying maps have a split coequalizer , every functor preserves the split diagram, including and . Since equalizes , it factors uniquely to the displayed action . Cancellation of the epimorphisms proves the unit and multiplication laws. Any algebra-valued map equalizing the pair factors through , and cancelling proves that its factor preserves the action. This establishes creation of that coequalizer.
New to topics? Read the docs here!