0.7.1 Products, pullbacks, and equalizers

0.7.1 Products, pullbacks, and equalizers

A product \(X\times Y\) comes with projections \(\pi _X:X\times Y\to X\) and \(\pi _Y:X\times Y\to Y\). For every pair \(f:Z\to X\), \(g:Z\to Y\), there is a unique map \(\langle f,g\rangle :Z\to X\times Y\) whose projections recover \(f\) and \(g\).

A pullback refines this idea. Given \(f:X\to Z\) and \(g:Y\to Z\), the pullback \(X\times _ZY\) represents pairs that agree after mapping to \(Z\):

Every other commutative cone into this cospan factors uniquely through the pullback.

In RADAR, a pullback can express the relation obtained by joining two typed views over a shared key. A learned geometric apex is not merely an embedding with low pairwise error; it is asked to realize the declared incidence and join relations.

An equalizer of \(f,g:X\rightrightarrows Y\) is an object \(E\to X\) selecting exactly the part of \(X\) on which \(f\) and \(g\) agree. In SID, compatible local families form an equalizer of two restriction maps: one route restricts the first local section to an overlap, and the other restricts the second.