The factorization system on a span category

Proof. Any span \(X \xleftarrow {l} U \xrightarrow {r} Y\) can be factored as a backwards map followed by a forwards map: \[ X \xleftarrow {l} U \xrightarrow {\mathrm {id}_U} U \qquad \text {followed by} \qquad U \xleftarrow {\mathrm {id}_U} U \xrightarrow {r} Y. \] It remains to check orthogonality. Let \(l' \colon B \to A\) be a backwards map (given by \(l \in C_L\)) and \(r' \colon X \to Y\) be a forwards map (given by \(r \in C_R\)). We need to show that the square of hom animae

is a pullback. Using the formula for hom animae in a span category (see Lemma 13.1.13), this square is equivalent to

The square involving only \(C_L\) is degenerate, hence a pullback square, and similarly for the square involving \(C_R\). We conclude that this square is a pullback square, finishing the proof. □