docs/echo-types: sync composition and roadmap with landed work (#18)

Two files updated to match what actually ships on main:

  composition.md
    §1 (Accumulation). Retitled "landed"; inlined the shipped Agda
    names (Echo-comp-iso-to / -from / -from-to / -to-from) and
    noted both round-trips are definitional.
    §3 (Cancellation). Retitled "partial (Agda-backed maps, iso
    deferred)"; documents the two shipped maps (cancel-iso-to
    needs s-left, cancel-iso-from needs s-right); flags the
    triangle-identity coherence as the blocker for the full iso;
    corrects the earlier wording that claimed a bare section on g
    suffices.
    §"Composition laws — compact statement". Row 1 marked Landed,
    row 3 marked Partial with deferred round-trips.
    §"What to formalise next". Items 1 and 2 struck through as
    landed; pentagon promoted to item 3; full cancel-iso with
    round-trips added as item 4 with its specific blocker.

  roadmap.md
    Formalisation section. Echo-comp-iso tagged [landed],
    cancel-iso tagged [partial] with deferred round-trips, pentagon
    promoted.
    Suggested immediate ordering. Step 2 struck through; pentagon
    inserted as the next concrete composition-track follow-up;
    subsequent steps re-numbered 3–8.

No content changes to overview.md, taxonomy.md, or examples.md. No code
changed; pure doc sync. No postulates.

https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

docs/echo-types/composition.md

@@ -26,49 +26,70 @@ the shadow level but not generally at the intensional core.
 
 ---
 
-## Accumulation — Agda-backed (base case)
+## Accumulation — Agda-backed (base case, landed)
 
 *Lemma.* For `f : A → B` and `g : B → C`, the type
 `Echo(g ∘ f) y` is canonically isomorphic to
 `Σ B (λ b → Echo(f) b × (g b ≡ y))`.
 
-*Proof sketch.* Σ-associativity plus propositional-equality
-rearrangement. In Agda terms, given
+*Proof.* Σ-associativity plus propositional-equality rearrangement.
+In Agda terms, given
 ```
-Echo f b      = Σ A (λ x → f x ≡ b)
-Echo g y      = Σ B (λ b → g b ≡ y)
+Echo f b       = Σ A (λ x → f x ≡ b)
+Echo g y       = Σ B (λ b → g b ≡ y)
 Echo (g ∘ f) y = Σ A (λ x → g (f x) ≡ y)
 ```
 the iso is witnessed by
 ```
-to   : Σ A (λ x → g (f x) ≡ y) → Σ B (λ b → Σ A (λ x → f x ≡ b) × (g b ≡ y))
-to (x , p)       = (f x , (x , refl) , p)
-from : Σ B (λ b → Σ A (λ x → f x ≡ b) × (g b ≡ y)) → Σ A (λ x → g (f x) ≡ y)
+to   (x , p)              = (f x , (x , refl) , p)
 from (b , (x , refl) , p) = (x , p)
 ```
-and both round-trips are `refl`. Formalisation is routine and not
-yet in the repo; it is the cleanest candidate for the next
-composition lemma to land.
+and both round-trips reduce to `refl` definitionally once the
+`refl` pattern has pinned the intermediate `b` to `f x`. Landed
+in `proofs/agda/Echo.agda` as `Echo-comp-iso-to`, `Echo-comp-iso-from`,
+`Echo-comp-iso-from-to`, `Echo-comp-iso-to-from` (all pinned in
+`Smoke.agda`).
 
 *Agda adjacency.* `Echo.map-over-comp` proves functoriality of the
 derived action on echoes; this is the morphism side of the same
-composition law. The *object-side* isomorphism above is not yet
-proved but is a straightforward next milestone.
+composition law. The object-side iso above and the morphism-side
+composition law together give a coherent two-level story for
+composition.
 
 ---
 
-## Cancellation — expected corollary
+## Cancellation — partial (Agda-backed maps, iso deferred)
 
-*Conjecture.* If `g : B → C` has a section `s : C → B` with
-`g ∘ s ≡ id`, then `Echo(g ∘ f) y ≃ Echo(f) (s y)` for every `y`.
+*Statement.* If `g : B → C` has a two-sided inverse `s : C → B`
+with `s-left : ∀ b → s (g b) ≡ b` and `s-right : ∀ y → g (s y) ≡ y`,
+then `Echo(g ∘ f) y` and `Echo(f) (s y)` are related by a canonical
+forward and backward map.
 
-*Rationale.* Composing with an injection loses no information, so
-the intermediate factor in the accumulation law collapses to a
-single witnessed point.
-
-*Status.* Not proved. Depends on the accumulation isomorphism plus
-a section lemma that the current repo has pieces of (see
-`no-section-weaken` in `EchoLinear` for the negative direction).
+*What is landed.* Two maps in `proofs/agda/Echo.agda`, each
+requiring only the relevant half of the iso structure:
+```
+cancel-iso-to   : (s-left  : ∀ b → s (g b) ≡ b) → Echo (g ∘ f) y → Echo f (s y)
+cancel-iso-from : (s-right : ∀ y → g (s y) ≡ y) → Echo f (s y)   → Echo (g ∘ f) y
+```
+Pinned in `Smoke.agda` as `cancel-iso-to`, `cancel-iso-from`.
+
+*What is deferred.* The round-trips that would promote these two
+maps to a full iso are *not* proved. Under `--without-K`, the two
+round-trips require a triangle-identity coherence between `s-left`
+and `s-right` (roughly `cong g (s-left b) ≡ s-right (g b)`), which
+is not a consequence of the two pointwise inverse laws alone — a
+bare "both-way inverse" is weaker than an equivalence in HoTT
+terms. The in-file comment in `Echo.agda` flags this explicitly.
+Options for the full iso: (a) an equivalence record that packages
+the triangle identity as a field, or (b) stdlib's
+`Function.Bundles.Inverse`.
+
+*Correction to earlier wording.* A bare section on `g` (i.e.,
+`s-right` only) is not enough to collapse the Σ-over-intermediate
+in the accumulation law; the earlier version of this section
+claimed otherwise. The correction is that both `s-left` and
+`s-right` are needed, and even then the full iso needs triangle
+coherence.
 
 ---
 
@@ -175,15 +196,18 @@ hypothetical 2-category of Q1. Not attempted.
 
 Collecting the above:
 
-1. **(Agda-backed) Base accumulation iso.**
-   `Echo(g ∘ f) y ≃ Σ B (λ b → Echo(f) b × (g b ≡ y))`.
+1. **(Landed) Base accumulation iso.**
+   `Echo(g ∘ f) y ≃ Σ B (λ b → Echo(f) b × (g b ≡ y))`. Proved in
+   `Echo.agda` as `Echo-comp-iso-{to, from, from-to, to-from}`.
 
 2. **(Agda-backed) Functorial action.** `map-over` respects
    composition: `map-over (g' , c₁) ∘ map-over (f' , c₂) ≡ map-over
    ((g' ∘ f') , coherence)`. Proved in `Echo.map-over-comp`.
 
-3. **(Expected) Cancellation.** `Echo(g ∘ f) y ≃ Echo(f) (s y)` when
-   `g` has a section `s`.
+3. **(Partial) Cancellation.** Forward and backward maps landed as
+   `cancel-iso-to` (needs `s-left`) and `cancel-iso-from` (needs
+   `s-right`). Round-trips deferred pending a triangle-identity
+   coherence or a stdlib `Function.Bundles.Inverse` shim.
 
 4. **(Open) Pentagon.** Three-fold composition associates.
 
@@ -198,19 +222,27 @@ Collecting the above:
 
 ## What to formalise next
 
-Ranked by unblock-value:
-
-1. **Base accumulation iso.** Single Agda proof, no new modules
-   needed. Would add `Echo-comp-iso` to `Echo.agda`.
-2. **Cancellation corollary.** One paragraph on top of (1).
-3. **Pentagon coherence.** Moderate proof, probably one more lemma.
-4. **Approximate-echo skeleton.** New module
+Ranked by unblock-value. (1) and (2) landed; (3) onwards is open.
+
+1. ~~**Base accumulation iso.**~~ Landed in `Echo.agda` as
+   `Echo-comp-iso-{to, from, from-to, to-from}`.
+2. ~~**Cancellation corollary.**~~ Partially landed as
+   `cancel-iso-to` / `cancel-iso-from`; full iso deferred pending
+   triangle-identity coherence (see §3 above).
+3. **Pentagon coherence.** Three-fold composition associates.
+   Moderate proof on top of `Echo-comp-iso`, probably one more
+   lemma. Next concrete follow-up on this track.
+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.
+5. **Approximate-echo skeleton.** New module
    `EchoApprox.agda` defining ε-echoes and restating (1) in the
    approximate setting. This is where axis 2 of the taxonomy gets
    teeth.
-5. **Decoration commuting.** Per-decoration lemmas in the existing
+6. **Decoration commuting.** Per-decoration lemmas in the existing
    `EchoGraded`, `EchoLinear`, `EchoIndexed` modules.
 
 None of these depend on the blocked Buchholz-WF / shared-binder
-work. All are Sonnet-class proofs; (4) is Opus 4.7 design and
+work. All are Sonnet-class proofs; (5) is Opus 4.7 design and
 Sonnet execution.

docs/echo-types/roadmap.md

@@ -46,14 +46,17 @@ Paths marked **[unblocked]** can proceed today. Paths marked
 
 ## Formalisation work — Agda, no bottleneck
 
-- **[unblocked]** `Echo-comp-iso` in `Echo.agda`: the accumulation
+- **[landed]** `Echo-comp-iso` in `Echo.agda`: the accumulation
   isomorphism `Echo(g ∘ f) y ≃ Σ B (λ b → Echo(f) b × (g b ≡ y))`.
-  Sonnet-class proof; see composition.md §1.
-- **[unblocked]** `Echo-comp-cancellation`: corollary for sectioned
-  `g`. Follows from the iso plus an existing section-lemma pattern
-  (`no-section-weaken` in `EchoLinear`).
+  Shipped as `Echo-comp-iso-{to, from, from-to, to-from}`; both
+  round-trips are definitional. See `composition.md` §1.
+- **[partial]** `cancel-iso-to` / `cancel-iso-from` in `Echo.agda`:
+  forward and backward maps for the cancellation corollary, each
+  needing only the relevant half of g's iso structure. Round-trips
+  are **deferred** pending a triangle-identity coherence or a stdlib
+  `Function.Bundles.Inverse` shim. See `composition.md` §3.
 - **[unblocked]** Pentagon coherence for three-fold composition.
-  Routine.
+  Routine proof on top of `Echo-comp-iso`; next concrete follow-up.
 - **[unblocked]** `EchoApprox.agda`: new module for ε-indexed echoes
   over a metric codomain. First-class taxonomy axis 2 artifact.
 - **[unblocked]** Per-decoration composition lemmas in `EchoGraded`,
@@ -146,19 +149,23 @@ tractable today:
 
 1. **Theory: axis 2 formal definition** — 1–2 days.
    Unblocks `EchoApprox.agda`, which is required for examples 6 and 10.
-2. **Agda: `Echo-comp-iso` + cancellation** — 1 day.
-   Concrete, compiling, unblocks the composition roadmap.
-3. **Gate 1 adjacency refresh against the new taxonomy** — 1 day.
+2. ~~**Agda: `Echo-comp-iso` + cancellation**~~ — landed. Accumulation
+   iso plus both cancellation maps now live in `Echo.agda`; the full
+   cancellation iso (with round-trips) is the first deferred item —
+   needs a triangle-identity coherence (see composition.md §3).
+3. **Agda: pentagon coherence for `Echo-comp-iso`** — 1 day. Next
+   natural follow-up on the composition track.
+4. **Gate 1 adjacency refresh against the new taxonomy** — 1 day.
    Cheap coherence pass on existing docs.
-4. **Theory: pick one axis-8 refinement and formalise it** — 1–2
+5. **Theory: pick one axis-8 refinement and formalise it** — 1–2
    days. Four candidates in `taxonomy.md` §8 (cost-indexed echo,
    graded access modality, decidability-respecting echo, witness-
    search abstract machine). Choosing commits the repo to one
    formal handle on computational vs information-theoretic access.
-5. **Agda: `EchoApprox.agda`** — 2–3 days. First artifact of axis 2.
-6. **Applications chapter: compiler-analysis residue** — 2 days.
+6. **Agda: `EchoApprox.agda`** — 2–3 days. First artifact of axis 2.
+7. **Applications chapter: compiler-analysis residue** — 2 days.
    Largest reader value; entirely unblocked.
-7. **Per-decoration composition lemmas** — 1 day each. Useful
+8. **Per-decoration composition lemmas** — 1 day each. Useful
    coverage.
 
 Steps 1–4 are ~5–6 days of honest work that require nothing from