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

## 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](https://claude.com/claude-code)

Author: hyperpolymath

docs/echo-types/composition.md

@@ -267,10 +267,13 @@ Ranked by unblock-value. (1) and (2) landed; (3) onwards is open.
 3. ~~**Pentagon coherence.**~~ Landed: projection-level
    (`-pent-B`, `-pent-echo` as `refl`) plus the full Σ-shape iso
    (`Echo-comp-pent-Σ-assoc-{to, from, from-to, to-from}`).
-4. **Full cancel-iso with round-trips.** Needs an equivalence
-   record that packages `s-left`, `s-right`, and the triangle
-   identity as three fields, or direct use of stdlib's
-   `Function.Bundles.Inverse`. Then the round-trip refls go through.
+4. ~~**Full cancel-iso with round-trips.**~~ Landed: `Echo.cancel-iso`
+   packages the four pieces (`cancel-iso-{to, from, from-to, to-from}`)
+   plus both triangle-identity coherences as a single
+   `Function.Bundles._↔_` record. Companion `Echo.Echo-comp-iso`
+   does the same for the unconditional accumulation iso (no
+   triangles needed). Built via stdlib's `mk↔ₛ′`; both round-trips
+   close on the existing pointwise lemmas.
 5. ~~**Approximate-echo skeleton.**~~ Landed in
    `EchoApprox.agda` with `EchoR ε f y`, `echo-approx-intro`,
    `echo-approx-relax`, and `echo-approx-compose` (additive under

proofs/agda/Echo.agda

@@ -308,3 +308,64 @@ Echo-comp-pent-Σ-assoc-to-from :
   Echo-comp-pent-Σ-assoc-to f g h
     (Echo-comp-pent-Σ-assoc-from f g h r) ≡ r
 Echo-comp-pent-Σ-assoc-to-from f g h (b , ef , p) = refl
+
+----------------------------------------------------------------------
+-- Equivalence-record packaging
+--
+-- The `cancel-iso-{to,from,from-to,to-from}` and
+-- `Echo-comp-iso-{to,from,from-to,to-from}` quartets above each
+-- pair into a stdlib `Function.Bundles._↔_` (bijection /
+-- bi-invertible map). The `cancel-iso` packager takes the two
+-- triangle-identity coherences as hypotheses (one per round-trip),
+-- as the round-trip lemmas themselves require; the
+-- `Echo-comp-iso` packager is unconditional (the round-trips
+-- there are pure pattern-matching).
+--
+-- The `↔` record from `Function.Bundles` is the standard
+-- categorical-equivalence object in stdlib v2: `to`, `from`,
+-- congruences (trivial under `_≡_`), and the two strict-inverse
+-- laws. Building this here gives downstream consumers a single
+-- structured object instead of a quintuple of named lemmas, and
+-- means the cancel-iso closes `composition.md` §4 ("Full
+-- cancel-iso with round-trips") cleanly.
+
+open import Function.Bundles using (_↔_; mk↔ₛ′)
+
+-- Per-fiber Echo-comp iso, packaged as a ↔. The accumulation
+-- iso is unconditional, so no extra hypotheses are needed.
+
+Echo-comp-iso :
+  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+  (f : A → B) (g : B → C) (y : C) →
+  Echo (g ∘ f) y ↔ Σ B (λ b → Echo f b × (g b ≡ y))
+Echo-comp-iso f g y =
+  mk↔ₛ′
+    (λ e → Echo-comp-iso-to   f g {y = y} e)
+    (λ r → Echo-comp-iso-from f g {y = y} r)
+    (λ r → Echo-comp-iso-to-from f g r)
+    (λ e → Echo-comp-iso-from-to f g e)
+
+-- Per-fiber cancel iso, packaged as a ↔. Requires both triangle
+-- identities; one triangle implies the other in HoTT but the
+-- adjustment is non-trivial path algebra, so both are taken as
+-- explicit hypotheses (matching `cancel-iso-from-to` and
+-- `cancel-iso-to-from`).
+--
+-- Closes `docs/echo-types/composition.md` §4 ("Full cancel-iso
+-- with round-trips") via the stdlib equivalence record.
+
+cancel-iso :
+  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+  (f : A → B) (g : B → C) (s : C → B)
+  (s-left  : ∀ b → s (g b) ≡ b)
+  (s-right : ∀ y → g (s y) ≡ y)
+  (triangle₁ : ∀ b → cong g (s-left b) ≡ s-right (g b))
+  (triangle₂ : ∀ y → cong s (s-right y) ≡ s-left (s y))
+  (y : C) →
+  Echo (g ∘ f) y ↔ Echo f (s y)
+cancel-iso f g s s-left s-right triangle₁ triangle₂ y =
+  mk↔ₛ′
+    (λ e → cancel-iso-to   f g s s-left  {y = y} e)
+    (λ e → cancel-iso-from f g s s-right {y = y} e)
+    (λ e → cancel-iso-to-from f g s s-left s-right triangle₂ e)
+    (λ e → cancel-iso-from-to f g s s-left s-right triangle₁ e)

proofs/agda/Smoke.agda

@@ -28,6 +28,8 @@ open import Echo using
   ; Echo-comp-pent-Σ-assoc-from
   ; Echo-comp-pent-Σ-assoc-from-to
   ; Echo-comp-pent-Σ-assoc-to-from
+  ; Echo-comp-iso
+  ; cancel-iso
   )
 open import EchoCharacteristic using (collapse; echo-true; echo-false; echo-true≢echo-false)
 open import EchoResidue using (EchoR; collapse-to-residue; strict-weakening-collapse; no-section-collapse-to-residue)