Add Echo-comp-iso: accumulation law for echo composition

Formalises the composition iso from docs/echo-types/composition.md §1:

  Echo (g ∘ f) y ≃ Σ B (λ b → Echo f b × (g b ≡ y))

Four names land in Echo.agda:

  Echo-comp-iso-to      : Echo (g ∘ f) y → Σ B (Echo f b × g b ≡ y)
  Echo-comp-iso-from    : Σ B (Echo f b × g b ≡ y) → Echo (g ∘ f) y
  Echo-comp-iso-from-to : from ∘ to ≡ id on Echo (g ∘ f) y
  Echo-comp-iso-to-from : to ∘ from ≡ id on Σ B (Echo f b × g b ≡ y)

`from` pattern-matches `refl` on the internal echo-equality to pin
the intermediate b to `f x`; after that, both round-trips are
definitional so the proof body is a single refl. This passes
`--without-K` because the refl-pattern determines a pattern variable
(b) from a computation (f x) rather than reducing a reflexive
equation on two matching variables.

Pinned in Smoke.agda. Full suite + Smoke both exit 0. No postulates.

This is the base accumulation law; downstream conjectures stated in
composition.md §Q1–Q6 (2-category coherence, pentagon, cancellation
under iso vs section, approximate-echo tolerance calculus,
decoration-commuting, recovery interaction) remain open.

https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK

Author: claude

proofs/agda/Echo.agda

@@ -4,7 +4,7 @@ module Echo where
 
 open import Level using (Level; _⊔_)
 open import Function.Base using (_∘_; id)
-open import Data.Product.Base using (Σ; _,_)
+open import Data.Product.Base using (Σ; _,_; _×_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; cong)
 
 -- Echo_f(y) := Σ (x : A) , (f x ≡ y)
@@ -63,3 +63,35 @@ map-square :
   (square : ∀ x → f' (u x) ≡ v (f x)) {y : B} →
   Echo f y → Echo f' (v y)
 map-square f f' u v square (x , p) = u x , trans (square x) (cong v p)
+
+-- Composition isomorphism: the echo of g ∘ f at y is canonically
+-- equivalent to a Σ over an intermediate b : B of (Echo f b × g b ≡ y).
+-- This is the accumulation law from docs/echo-types/composition.md §1:
+-- composition does not weaken the intensional core, it accumulates
+-- witness structure. Both round-trips are definitional once the
+-- refl pattern has pinned the intermediate b to f x.
+
+Echo-comp-iso-to :
+  ∀ {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-to f g (x , p) = f x , (x , refl) , p
+
+Echo-comp-iso-from :
+  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+  (f : A → B) (g : B → C) {y : C} →
+  Σ B (λ b → Echo f b × (g b ≡ y)) → Echo (g ∘ f) y
+Echo-comp-iso-from f g (b , (x , refl) , p) = x , p
+
+Echo-comp-iso-from-to :
+  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+  (f : A → B) (g : B → C) {y : C} (e : Echo (g ∘ f) y) →
+  Echo-comp-iso-from f g (Echo-comp-iso-to f g e) ≡ e
+Echo-comp-iso-from-to f g (x , p) = refl
+
+Echo-comp-iso-to-from :
+  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+  (f : A → B) (g : B → C) {y : C}
+  (r : Σ B (λ b → Echo f b × (g b ≡ y))) →
+  Echo-comp-iso-to f g (Echo-comp-iso-from f g r) ≡ r
+Echo-comp-iso-to-from f g (b , (x , refl) , p) = refl

proofs/agda/Smoke.agda

@@ -6,7 +6,18 @@
 
 module Smoke where
 
-open import Echo using (Echo; echo-intro; map-over; map-over-id; map-over-comp; map-square)
+open import Echo using
+  ( Echo
+  ; echo-intro
+  ; map-over
+  ; map-over-id
+  ; map-over-comp
+  ; map-square
+  ; Echo-comp-iso-to
+  ; Echo-comp-iso-from
+  ; Echo-comp-iso-from-to
+  ; Echo-comp-iso-to-from
+  )
 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)
 open import EchoExamples using (square9; visible; quot; collapse-residue-identifies)