Commit 2020-12-08 15:28 7f5a5ddd

feat(category_theory/limits): split coequalizers (#5230) Define what it means for a triple of morphisms f g : X ⟶ Y, π : Y ⟶ Z to be a split coequalizer, and show that every split coequalizer is a coequalizer and absolute. Define split pairs and G-split pairs. These definitions and constructions are useful in particular for the monadicity theorems.