agda(Echo): equivalence-record packaging for cancel-iso (closes composition.md §4)

[hyperpolymath]

Summary

• Adds two equivalence-record packagers in `Echo.agda` using stdlib's `Function.Bundles.↔` and `mk↔ₛ′`:
  • `Echo-comp-iso` — unconditional accumulation iso `Echo (g ∘ f) y ↔ Σ B (λ b → Echo f b × g b ≡ y)`, built from the existing `Echo-comp-iso-{to,from,from-to,to-from}` quartet.
  • `cancel-iso` — per-fiber cancellation equivalence `Echo (g ∘ f) y ↔ Echo f (s y)`, parameterised by `s-left`, `s-right`, and both triangle-identity coherences (`triangle₁`, `triangle₂`); built from the existing `cancel-iso-{to,from,from-to,to-from}` quartet.
• Closes `docs/echo-types/composition.md` §4 ("Full cancel-iso with round-trips") cleanly. Each triangle is needed for the corresponding round-trip — one implies the other in HoTT but the adjustment is non-trivial path algebra, so both stay explicit.
• Pinned in `Smoke.agda`.

Why

The four cancel-iso pieces had been load-bearing as separate lemmas, requiring downstream consumers to apply them in tandem to recover the equivalence shape. Packaging them into a single `↔` record gives one structured object (with strict-inverse laws available via `mk↔ₛ′`'s field projections) and matches stdlib's idiom for bi-invertible maps.

Compile-verification

```
agda -i proofs/agda proofs/agda/All.agda
agda -i proofs/agda proofs/agda/Smoke.agda
```

Both exit 0 under `--safe --without-K`. No postulates introduced.

Test plan

• `agda -i proofs/agda proofs/agda/All.agda` exits 0
• `agda -i proofs/agda proofs/agda/Smoke.agda` exits 0
• `grep -n postulate proofs/agda/Echo.agda` returns nothing
• `Echo-comp-iso` and `cancel-iso` headlines pinned in `Smoke.agda`

🤖 Generated with Claude Code