A.6.2:4.3.5 - P4 — Arrow and repeat boundary

The common EFEM model treats f : X -> Y as one arrow with exact endpoints, an arrow rule or designator, and declared formal equivalence. It does not treat every arrow as a function that can be evaluated on an object, and it makes no claim that a separately declared operation is deterministic. A concrete substrate may add an evaluation operation only after declaring its argument kind, result kind, and relation to these exact arrows; that extra operation is not part of the common EFEM laws.

No universal idempotence follows. A normalization or another endomorphism f : X -> X may separately claim a repeat law such as compose(f,f) ≃ f only when composition is defined on the declared domain, ≃ is the substrate’s stated equivalence, and a working fixture or proof supplies the witness. This mathematical repeat claim is not evidence that an operation was executed twice.