lin-0108
8.4 Transport through backpropagation
Let \(\mathcal L_{\varepsilon ,e}\) denote the learner construction determined by a loss \(e\) and step size \(\varepsilon \). If it is functorial and strong monoidal, then a satisfied architectural equation is transported:
Suppose \(D\) is a strong symmetric monoidal candidate and \(\mathcal L_{\varepsilon ,e}:\mathbf{Para}\to \mathbf{Learn}\) is a strong symmetric monoidal functor. If \(D\) factors through the equation quotient \(q\), then \(\mathcal L_{\varepsilon ,e}D\) also factors through \(q\).
Equal formal paths have equal images under \(D\). Functoriality preserves their equality under \(\mathcal L_{\varepsilon ,e}\), and strong monoidality preserves the declared parallel wiring.
The converse need not hold, and equality of forward implementations need not force equality of arbitrary hand-designed update rules. The proposition depends on using the declared functorial learner construction.
Forward agreement, tangent agreement, update agreement, and request agreement are four different audits. They coincide only under hypotheses supplied by the realization.