Idempotent splitting through a coequalizer
ID: idempotent-splitting-through-a-coequalizer
If and , then is the coequalizer of : an arrow with factors uniquely as . Conversely a coequalizer makes factor as ; epimorphic cancellation gives . Thus the splitting of an idempotent morphism is equivalent to this particular coequalizer, without assuming arbitrary coequalizers exist.
New to topics? Read the docs here!