MATH.12:5.2 - Read a function equivalence as two transformations

Suppose f maps each a in A to a pair in B×C. A proof can split this into two functions by projecting its output:

Split(f) = (a ↦ first(f(a)), a ↦ second(f(a))).

Conversely, given g:A→B and h:A→C, pair their values:

Join(g,h) = a ↦ (g(a),h(a)).

Applying Join after Split gives, at each a:

(first(f(a)),second(f(a))) = f(a).

Applying Split after Join returns g and h pointwise. Thus the argument supplies transformations in both directions, together with the equalities that justify using the returned functions.

For f(n)=(n+1,n^2), Split gives g(n)=n+1 and h(n)=n^2. Joining their values at n=3 returns (4,9). The projections and applications are the computational content of the proof.

The equality concerns functions with values determined by their input. If evaluating f is expensive, the expression using two calls can repeat work; calculate f(a) once and keep its pair when both components are needed.

If the proposed implementation instead reads and increments a hidden counter, repeated calls change the situation. A single call returning (c,c) might give (1,1), while separate component calls yield (1,2). This no longer implements the fixed mathematical f used by the proof. Include the changing state in the model and reconsider the transformation before using this function equivalence to reorganize the work.