Monomorphism that is Split Epimorphism is Split Monomorphism

Theorem

Let $\mathbf C$ be a metacategory.

Let $f: C \to D$ be a morphism in $\mathbf C$ such that $f$ is a monomorphism and a split epimorphism.

Then $f: C \to D$ is a split monomorphism.

Proof

Let $g: D \to C$ be the right inverse of $f$:

$f \circ g = \operatorname{id}_D$

which is guaranteed to exist by definition of split epimorphism.

Therefore:

$f \circ g \circ f = \operatorname{id}_D \circ f = f \circ \operatorname{id}_C$

by the property of the identity morphism.

Since $f$ is left cancellable, by the definition of monomorphism, we have:

$g \circ f = \operatorname{id}_C$

Hence $f$ is a split monomorphism with left inverse $g$.

$\blacksquare$