Proposition: Domain-sensitive transfer

Let $A$ be an identity proved for signature ${\Sigma }_1$ on domain ${\mathcal{C}}_1$. To transfer that identity to an object with signature ${\Sigma }_2$ and domain ${\mathcal{C}}_2$, it suffices to provide maps transporting all operations and arguments used in $A$, together with proofs that:

1. the target arguments belong to the transported domain;

2. the transported operations agree with the target operations;

3. all products, pullbacks, quotients, and limits used in the transport are defined;

4. the normalization and perturbative grading are respected.

Without such a bridge, the identity for ${\Sigma }_1$ supplies no domain-independent transfer theorem for ${\Sigma }_2$.

Proof. Under the four hypotheses, replace each argument and operation in the proved identity by its transported counterpart. The intertwining identities preserve the equality, and the domain hypotheses justify every operation.

For the final assertion, an equality on ${\mathcal{C}}_1$ alone does not specify operations or values on ${\mathcal{C}}_2$. If ${\mathcal{C}}_2$ contains additional arguments, the operations can agree on the transported part and differ elsewhere without contradicting the original equality. If no transport is specified, one may regard the two carriers as independently tagged copies; the original identity then contains no statement identifying their operations. Consequently a transfer conclusion requires additional premises. This is a statement about the scope of the given identity, not a theorem that no bridge can exist.