CatDat

Implication Details

Assumptions: equalizers

Conclusions: Cauchy complete

Reason: If $e : X \to X$ is an idempotent, then the equalizer of $e, \mathrm{id}_X : X \rightrightarrows X$ provides a splitting of $e$.