MATH.18:4.4 - Construct the return and examine the composites

When two-way use is needed, construct a return interpretation G. Apply G∘F to source ingredients and F∘G to target ingredients. Inspect what each round trip returns.

Sometimes the ingredients are recovered literally, as in the order-and-operation case below. Sometimes a specified isomorphism supplies recovery: an invertible map preserving the structure used by the comparison.

When whole systems of objects and maps are compared, pointwise isomorphisms need compatibility with the maps. If eta_A:A -> G(F(A)) provides source recovery, require for every source map f:A -> B:

G(F(f))∘eta_A = eta_B∘f.

Both routes start in A and finish in G(F(B)). This equation means that translating and then applying the map agrees with applying the map and then translating. Require the corresponding compatibility on the target side as well. In categorical language, functors with these natural isomorphisms give an equivalence of categories.

Use that equivalence for properties supported by the chosen structure and invariant under its isomorphisms. If a later question uses additional structure, include it in the comparison. The length question in :5.3 shows why this return matters.

If only one direction is constructed or needed, retain that useful interpretation at its established scope. If two-way recovery fails, name the unrecovered operation, assertion or distinction that matters to the work.