agda(Echo): equivalence-record packaging for cancel-iso + Echo-comp-iso

Closes docs/echo-types/composition.md §4 ("Full cancel-iso with
round-trips") via stdlib's `Function.Bundles._↔_`.

Two new headlines (pinned in Smoke.agda):

  * Echo-comp-iso : (f : A → B) (g : B → C) (y : C) →
                    Echo (g ∘ f) y ↔ Σ B (λ b → Echo f b × g b ≡ y)
    Unconditional accumulation iso, packaged from the existing
    Echo-comp-iso-{to, from, from-to, to-from} via mk↔ₛ′.

  * cancel-iso : (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)
    Per-fiber cancellation equivalence, requiring both triangle
    identities. Built from cancel-iso-{to, from, from-to, to-from}
    via mk↔ₛ′. 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.

Verification: agda proofs/agda/All.agda and agda proofs/agda/Smoke.agda
both exit 0 under --safe --without-K. No postulates introduced.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

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)