= Solution
The equality predicate on $A$ is interpreted by the diagonal <monomorphism> $\Delta_A:A\hookrightarrow A\times A$. The antecedent equality of the two $f$-values is the <kernel pair> $A\times_BA\hookrightarrow A\times A$. Semantic validity of the implication says that the kernel-pair subobject is contained in the diagonal; the reverse containment always holds. Hence the sequent is valid exactly when
$$
A\times_BA=\Delta_A.
$$
If $f$ is monic, this equality is its cancellation property expressed by the pullback. Conversely, if $fr=fs$ for $r,s:X\to A$, then $(r,s)$ factors through this kernel pair and therefore through the diagonal, giving $r=s$. Thus \b[the sequent holds exactly when the map is a monomorphism]. This argument uses generalized arrows from arbitrary $X$, not a claim that global elements detect maps.
Back to article page
