|
1 | 1 | # Is this just Sigma Types? |
2 | 2 |
|
3 | 3 | ## The Skeptical Position |
4 | | -Yes, at the lowest level of Agda code, this is `Σ (x : A) , (f x ≡ y)`. It relies entirely on the standard dependent pair type and propositional equality. |
| 4 | +Yes, at the lowest level of Agda code, this is `Σ (x : A) , (f x ≡ y)`. |
| 5 | +It relies entirely on the standard dependent pair type and propositional |
| 6 | +equality. |
5 | 7 |
|
6 | 8 | ## The Burden of Proof |
7 | | -Any claim of utility must show why working with the `Echo` wrapper is better than directly pattern-matching on the Sigma type. If every proof immediately unpacks the `Echo` and does standard Sigma-type manipulation, the abstraction is leaky and pointless. |
| 9 | +Any claim of utility must show why working with the `Echo` wrapper is |
| 10 | +better than directly pattern-matching on the Sigma type. If every proof |
| 11 | +immediately unpacks the `Echo` and does standard Sigma-type manipulation, |
| 12 | +the abstraction is leaky and pointless. |
8 | 13 |
|
9 | 14 | ## Collapse Conditions |
10 | | -If the `Echo` interface requires the user to manually manage the underlying `Σ` structure to accomplish basic composition or mapping tasks, the abstraction fails. |
| 15 | +If the `Echo` interface requires the user to manually manage the |
| 16 | +underlying `Σ` structure to accomplish basic composition or mapping |
| 17 | +tasks, the abstraction fails. |
11 | 18 |
|
12 | 19 | ## Reinterpretation vs. Novelty |
13 | | -The novelty must reside in the API and the categorical/compositional properties exposed by the wrapper, demonstrating that `Echo` behaves coherently under lossy operations in a way that bare Sigma types do not automatically communicate. |
| 20 | +The novelty must reside in the API and the categorical/compositional |
| 21 | +properties exposed by the wrapper, demonstrating that `Echo` behaves |
| 22 | +coherently under lossy operations in a way that bare Sigma types do not |
| 23 | +automatically communicate. |
| 24 | + |
| 25 | +--- |
| 26 | + |
| 27 | +## Answer: the in-tree evidence |
| 28 | + |
| 29 | +This section is the index reviewers can walk to confirm Echo is not |
| 30 | +"renamed Σ". It is organised under five demands a sceptic typically |
| 31 | +makes. Each item points at a machine-checked Agda artefact (pinned in |
| 32 | +`proofs/agda/Smoke.agda`), a doc, or both. Statements stay inside the |
| 33 | +*narrowed* claims of `docs/retractions.adoc` R-2026-05-18 — no "full |
| 34 | +universal property", no "graded comonad", no "model-independence". |
| 35 | + |
| 36 | +### 1. Irreversibility is a theorem family, not a property |
| 37 | + |
| 38 | +A raw `Σ (x : A) (f x ≡ y)` gives `proj₁` trivially; the user can |
| 39 | +always extract the original `x`. The Echo programme proves that *no* |
| 40 | +section exists once specific lossy interfaces are applied. The witness |
| 41 | +is a *family* across five separate decoration layers: |
| 42 | + |
| 43 | +- `EchoCharacteristic.no-section-collapse` — no section of the |
| 44 | + `Bool → ⊤` collapse map. |
| 45 | +- `EchoCharacteristic.no-section-visible` — no section recovering the |
| 46 | + pre-image from a visible output alone. |
| 47 | +- `EchoResidue.no-section-collapse-to-residue` — weakening to a residue |
| 48 | + is provably one-way. |
| 49 | +- `EchoLinear.no-section-weaken` — the `linear → affine` mode shift is |
| 50 | + one-way (defined as the residue lemma). |
| 51 | +- `EchoOrdinal.no-section-ordinal-collapse` — ordinal collapse case. |
| 52 | +- `EchoEpistemicResidue.no-section-to-epistemic` — epistemic-residue |
| 53 | + case. |
| 54 | + |
| 55 | +All six are pinned in `Smoke.agda`. The family is what carries the |
| 56 | +weight: each decoration *separately* refuses the section that a raw Σ |
| 57 | +would admit. See also `docs/theorem-index.md` and the prose write-up at |
| 58 | +`docs/characteristic.adoc`. |
| 59 | + |
| 60 | +### 2. Loss is graded, and downgrades cannot be reversed |
| 61 | + |
| 62 | +A raw Σ has no built-in notion of "degrading from strict to loose". |
| 63 | +Echo equips the fibre with a lattice of grades and a monotone reindexing |
| 64 | +along it. The two halves of the asymmetry are: |
| 65 | + |
| 66 | +- *Down-step is admissible.* `EchoGraded.degrade-compose` and |
| 67 | + `EchoGraded.degrade-via-join` — the per-decoration composition law |
| 68 | + for the loss-grade order. Same recipe lands at: |
| 69 | + - `EchoLinear.degradeMode-compose` (linearity-mode order), |
| 70 | + - `EchoChoreo.applyChoreo-compose` (role/reachability order), |
| 71 | + - `EchoAccess` (graded access modality), |
| 72 | + - `EchoCost` (cost-indexed refinement), |
| 73 | + - `EchoSearch` (witness-search refinement). |
| 74 | +- *Up-step is not.* `no-section-weaken` (item 1) is the same |
| 75 | + statement on the other diagonal — once degraded, no inverse exists. |
| 76 | + |
| 77 | +Honest framing: this is a *thin-poset reindexing modality*, not a |
| 78 | +graded comonad. The retraction at `docs/retractions.adoc#R-2026-05-18` |
| 79 | +narrowed an earlier "graded comonad" claim. The reindexing modality is |
| 80 | +the load-bearing structure and is the right answer to "is Σ enough?": |
| 81 | +Σ alone gives neither the monotone reindex nor the no-section dual. |
| 82 | + |
| 83 | +### 3. Echo is the homotopy fibre; bridges from other "loss-tracker" frameworks exist |
| 84 | + |
| 85 | +The categorical/identity claim is **deflationary** and owned in |
| 86 | +`docs/echo-types/establishment-plan.adoc`: `Echo f y` is *definitionally* |
| 87 | +the homotopy fibre `fib f y` (HoTT book Def. 4.2.4). The bridge is |
| 88 | +`EchoFiberBridge.echo↔fib`, both round-trips `refl` (Pillar A; pinned |
| 89 | +in `Smoke.agda`). |
| 90 | + |
| 91 | +For the "is this just a pullback" question, `EchoPullback.echo-pullback-univ` |
| 92 | +exhibits `Echo f y` as the pullback of `f` along `y : ⊤ → B` with a |
| 93 | +*pointwise, funext-relative* mediator property. The retraction note in |
| 94 | +that module is loud: this is **not** a full categorical universal |
| 95 | +property in the absence of funext. Bridges from named neighbour |
| 96 | +frameworks land as separate modules: |
| 97 | + |
| 98 | +- `EchoFiberBridge.agda` — homotopy fibre identity. |
| 99 | +- `EchoJanusBridge.agda` — Janus-style reversible debugger bridge. |
| 100 | +- `EchoTropical.agda` / `AntiEchoTropical.agda` — tropical |
| 101 | + semiring / argmin decomposition. |
| 102 | +- `EchoCNOBridge.agda` — categorical neighbour bridge. |
| 103 | +- `EchoFiberCount.agda` + `EchoThermodynamics*.agda` — finite-fibre |
| 104 | + Landauer / Bennett correspondence. |
| 105 | + |
| 106 | +These are independent witnesses, not one universal theorem. The honest |
| 107 | +verdict is "Echo is *a* canonical target with concrete bridges in" |
| 108 | +rather than "Echo is *the* terminal residue tracker by unique mediator". |
| 109 | + |
| 110 | +### 4. The abstraction barrier (consumer-side) |
| 111 | + |
| 112 | +A raw `Σ A (λ x → f x ≡ y)` exposes `proj₁`, so a consumer can always |
| 113 | +distinguish two preimages of the same output. The Echo interface at the |
| 114 | +affine mode does not export that projection: the residue carrier is |
| 115 | +contractible (`EchoLinear.affine-canonical`, `affine-all-equal`), so |
| 116 | +any consumer assigns the same value to the weakened images of two |
| 117 | +known-distinct linear echoes. |
| 118 | + |
| 119 | +**Status:** the consumer-side abstraction-barrier theorem is the one |
| 120 | +genuine gap relative to the five demands. It is planned as |
| 121 | +`proofs/agda/EchoAbstractionBarrier.agda` (Track B in the work plan). |
| 122 | +The model-side counterpart — *carrier-parametricity* over a fixed |
| 123 | +grade poset — already lands as `EchoRelModel` (Pillar D, narrowed per |
| 124 | +R-2026-05-18 from the original "model-independence" wording). |
| 125 | + |
| 126 | +### 5. Canonical examples — what Σ would let through |
| 127 | + |
| 128 | +The example modules exhibit echo as the explanatory unit on real |
| 129 | +artefacts: |
| 130 | + |
| 131 | +- `EchoExampleParser` — `(())` vs `()()` are two distinct echoes at the |
| 132 | + same `parses ≡ true`. |
| 133 | +- `EchoExampleProvenance` — distinct Bool-provenance rows collapse to |
| 134 | + the same payload; the echo carries the lost annotation. |
| 135 | +- `EchoExampleAbsInt` — `{p1, p2}` collapse to `pos` under sign |
| 136 | + analysis; the echo retains which. |
| 137 | +- `EchoExampleSignAnalysis`, `EchoExampleTruncation` — further |
| 138 | + collapse-with-residue exhibits. |
| 139 | +- `EchoFiberCount` + `EchoThermodynamics*` — finite-fibre Landauer |
| 140 | + bound for the erasure cost. |
| 141 | +- `EchoEpistemicResidue` — observation-discipline residue. |
| 142 | + |
| 143 | +Each is positive evidence. The matched *negative* — a small raw-Σ |
| 144 | +counter-program that would let the bug through — is planned as |
| 145 | +`proofs/agda/examples/EchoVsSigma.agda` (Track C). Until that lands, |
| 146 | +the "raw Σ would leak" claim is prose, not a checked artefact. |
| 147 | + |
| 148 | +--- |
| 149 | + |
| 150 | +## Cross-references |
| 151 | + |
| 152 | +- Gate 2 audit (closest reviewer touchpoint): |
| 153 | + `docs/characteristic.adoc`. |
| 154 | +- Theorem-by-theorem ledger: `docs/theorem-index.md`. |
| 155 | +- Adjacency notes (per neighbour framework): `docs/adjacency/`. |
| 156 | +- Honest scope of the establishment claim: |
| 157 | + `docs/echo-types/establishment-plan.adoc` and |
| 158 | + `docs/echo-types/paper.adoc` §"Reframing note". |
| 159 | +- AsciiDoc reviewer companion to this file: |
| 160 | + `docs/echo-types/sigma-distinctness-map.adoc`. |
| 161 | +- Companion skepticisms: `is-this-just-fibers.md`, `what-is-actually-new.md`, |
| 162 | + `failure-conditions.md`. |
0 commit comments