CatDat

Implication Details

Assumptions: preadditive, quotients of congruences, regular

Conclusions: cokernels

Reason: By the regularity assumption, it suffices to consider cokernels of subobjects. Given a subobject $Y$ of $X$, we have the congruence on $X$ given by the pullback of ${-} : X \times X \to X$ and $Y$. The quotient of this congruence is a cokernel of $Y \hookrightarrow X$.