MATH.5:4.4 - Make the map respect identified expressions

If the source equates expressions, test the equations under E. To define E_bar([t])=E(t) on an equivalence class, require:

t~u implies E(t)=E(u).

MATH.2 supplies the quotient and representative-independence construction. Here it is applied to the evaluation just obtained.

For typed paths with the objects retained, impose equations between paths having the same source and target. Compare their target arrows, including the appropriate identity for an empty path. Closure under permitted composition makes the evaluation descend just as above. Identifying different source objects changes this setup and requires a construction that also accounts for their identities and permitted joins.

When the source equivalence is generated by stated equations and their use inside larger expressions, show that each generating equation has equal evaluated sides. Equality is preserved when equal values enter the same target operation. It is also preserved along reversal and a finite sequence of equation replacements. These facts extend the result to the generated equivalence.

An equation schema such as s*t=t*s ranges over its permitted substitutions. Checking one numerical substitution leaves the other instances unresolved. Establish the target law for the required range or return a failing instance. If the source also has additional identifications, include them in the comparison.

A failed equation gives a concrete choice: change the generator assignment, change the target operations, or use a source construction that retains the distinction. Each option changes the mathematical account. Select the one that still answers the receiving question.