Categorical diagonal (source code)

= Categorical diagonal
{title2=$\Delta_A$}

For a binary <product in a category>, the diagonal $\Delta_A:A\to A\times A$ is the unique map whose two projection composites are $1_A$. It is a <split monomorphism>, since either projection is a left inverse. The diagonal converts equality of two maps into a lifting problem: $\langle u,v\rangle$ factors through $\Delta_A$ exactly when $u=v$.