Merge remote-tracking branch 'origin/main'

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

proofs/agda/Echo.agda

@@ -4,8 +4,8 @@ module Echo where
 
 open import Level using (Level; _⊔_)
 open import Function.Base using (_∘_; id)
-open import Data.Product.Base using (Σ; _,_; _×_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; cong)
+open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)
 
 -- Echo_f(y) := Σ (x : A) , (f x ≡ y)
 Echo : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → B → Set (a ⊔ b)
@@ -95,3 +95,77 @@ Echo-comp-iso-to-from :
   (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
+
+-- Cancellation corollary: when g is a bijection with inverse s
+-- (both s-right : g ∘ s ≡ id and s-left : s ∘ g ≡ id, pointwise),
+-- Echo (g ∘ f) y is equivalent to Echo f (s y). This is the
+-- conjecture from composition.md, restated in the corrected form
+-- (a bare section on g is not enough — you need both sides of the
+-- iso to collapse the Σ-over-intermediate in the accumulation law).
+
+cancel-iso-to :
+  ∀ {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)
+  {y : C} →
+  Echo (g ∘ f) y → Echo f (s y)
+cancel-iso-to f g s s-left (x , p) = x , trans (sym (s-left (f x))) (cong s p)
+
+cancel-iso-from :
+  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+  (f : A → B) (g : B → C) (s : C → B)
+  (s-right : ∀ y → g (s y) ≡ y)
+  {y : C} →
+  Echo f (s y) → Echo (g ∘ f) y
+cancel-iso-from f g s s-right {y = y} (x , q) =
+  x , trans (cong g q) (s-right y)
+
+-- The two maps above witness that `Echo (g ∘ f) y` and `Echo f (s y)`
+-- are *related* via g's section/retraction structure. To conclude
+-- they are *isomorphic* one must also prove two round-trips equal to
+-- the identity. Under `--without-K`, that requires 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 laws alone — a bare "both-way inverse" is weaker
+-- than an equivalence / bijection in HoTT terms. The round-trip
+-- formalisation is deferred until we commit to either (a) an
+-- equivalence record that packages the triangle identity as a field,
+-- or (b) stdlib's `Function.Bundles.Inverse`.
+
+-- Pentagon coherence for three-fold composition. Given
+-- f : A → B, g : B → C, h : C → D, the echo of (h ∘ g ∘ f)
+-- admits two natural factorings via `Echo-comp-iso-to`:
+--
+--   outer-first : split at outer boundary (h) then at inner (g)
+--       Echo (h ∘ (g ∘ f)) y
+--     → Σ C (λ c → Echo (g ∘ f) c × (h c ≡ y))         [iso on (g∘f, h)]
+--     → Σ C (λ c → Σ B (λ b → Echo f b × (g b ≡ c)) × (h c ≡ y))
+--
+--   inner-first : split at the inner boundary ((h∘g) as outer, f as inner)
+--       Echo ((h ∘ g) ∘ f) y
+--     → Σ B (λ b → Echo f b × ((h ∘ g) b ≡ y))         [iso on (f, h∘g)]
+--
+-- Both factorings project to the same `f x` at the B-component and
+-- the same `x , refl` at the Echo-f witness. This is the minimal
+-- pentagon-style coherence: the two natural applications of
+-- Echo-comp-iso agree on the A-origin of the composite echo.
+
+Echo-comp-iso-pent-B :
+  ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
+  (f : A → B) (g : B → C) (h : C → D) {y : D}
+  (e : Echo (h ∘ g ∘ f) y) →
+  proj₁ (Echo-comp-iso-to f g
+           (proj₁ (proj₂ (Echo-comp-iso-to (g ∘ f) h e))))
+  ≡ proj₁ (Echo-comp-iso-to f (h ∘ g) e)
+Echo-comp-iso-pent-B f g h (x , p) = refl
+
+-- Stronger statement: same `(x , refl) : Echo f (f x)` on the
+-- Echo-f component too.
+Echo-comp-iso-pent-echo :
+  ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
+  (f : A → B) (g : B → C) (h : C → D) {y : D}
+  (e : Echo (h ∘ g ∘ f) y) →
+  proj₁ (proj₂ (Echo-comp-iso-to f g
+                  (proj₁ (proj₂ (Echo-comp-iso-to (g ∘ f) h e)))))
+  ≡ proj₁ (proj₂ (Echo-comp-iso-to f (h ∘ g) e))
+Echo-comp-iso-pent-echo f g h (x , p) = refl

proofs/agda/Smoke.agda

@@ -17,6 +17,10 @@ open import Echo using
   ; Echo-comp-iso-from
   ; Echo-comp-iso-from-to
   ; Echo-comp-iso-to-from
+  ; cancel-iso-to
+  ; cancel-iso-from
+  ; Echo-comp-iso-pent-B
+  ; Echo-comp-iso-pent-echo
   )
 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)