From 8c9ddcb1d2ef3e6f29cc7eb53cd2e21f904dd670 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 18 May 2026 04:16:12 +0100
Subject: [PATCH 1/3] harden(foundation P1): reproducible CI-via-flake exact
 pin (additive verifier)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

flake.nix evolved to pin the toolchain reproducibly:
  * Agda via nixpkgs nixos-24.11 (2.7.0.1)
  * standard-library tag v2.3 as a flake input (was nixpkgs-bundled,
    a DIFFERENT version than CI/local verify against)
  * absolute-zero @3ff5cee as a flake input (was a local ~/dev
    checkout — not reproducible / not CI-usable)
plus a hermetic checks.suite (guardrail + 4 roots + N5 xfail) under
that pinned toolchain.

CI: additive  job runs . ADDITIVE and
continue-on-error: the apt  +  jobs remain the
gate, so the 2.7.0.1-vs-verified-2.8.0 delta (if any) is SURFACED,
not a regression. First green run is the P1 verification.

Honest constraints, flagged not hidden (triage, not a blind cutover):
  * no  in the dev env → flake authored designed-correct,
    verified BY CI, NOT locally claimed green; libraries file built
    via writeText+cp (no heredoc/indentation hazard) to de-risk the
    one fragile part by construction.
  * cross-stack: a devShell-only flake.nix also lives on the reframe
    stack (#47, commit 185eb74); THIS strictly supersedes it (adds
    pins+checks, no behavioural conflict) — take this at integration.
  * Agda 2.7.0.1 vs verified 2.8.0 is an explicit surfaced decision,
    not an assumption; reconcile via the logged CI delta.

docs/foundation.adoc P1 item moved tracked-followup -> implemented,
pending first-green CI verification; revision history appended.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 .github/workflows/agda.yml |  25 ++++++++
 docs/foundation.adoc       |  34 +++++++++--
 flake.nix                  | 117 +++++++++++++++++++++++++++++++++++++
 3 files changed, 170 insertions(+), 6 deletions(-)
 create mode 100644 flake.nix

diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml
index 93fc6cc..29196fa 100644
--- a/.github/workflows/agda.yml
+++ b/.github/workflows/agda.yml
@@ -179,3 +179,28 @@ jobs:
           agda --ignore-interfaces -i proofs/agda proofs/agda/Smoke.agda
           agda --ignore-interfaces -i proofs/agda proofs/agda/characteristic/All.agda
           agda --ignore-interfaces -i proofs/agda proofs/agda/examples/All.agda
+
+  flake-check:
+    # Foundation P1: the reproducible, exactly-pinned toolchain.
+    # `nix flake check` runs flake.nix's hermetic `checks.suite`
+    # (flake-pinned Agda + PINNED stdlib v2.3 + PINNED absolute-zero
+    # @3ff5cee, guardrail + 4 roots + N5 xfail). ADDITIVE: the apt
+    # `check` and `cold-check` jobs remain the gate, so a version
+    # delta surfaced here (e.g. 2.7.0.1 vs verified 2.8.0) is
+    # informative, not a regression. Its first green run IS the P1
+    # verification (the dev env has no nix; CI is the verifier).
+    # Flip continue-on-error to false once it is first green.
+    runs-on: ubuntu-latest
+    continue-on-error: true
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+
+      - name: Install Nix (pinned action)
+        uses: cachix/install-nix-action@08dcb3a5e62fa31e2da3d490afc4176ef55ecd72  # v30
+        with:
+          extra_nix_config: |
+            experimental-features = nix-command flakes
+
+      - name: nix flake check (hermetic, reproducible)
+        run: nix flake check --print-build-logs
diff --git a/docs/foundation.adoc b/docs/foundation.adoc
index 064b3fb..fca1320 100644
--- a/docs/foundation.adoc
+++ b/docs/foundation.adoc
@@ -89,12 +89,25 @@ hack: left explicit and failing, never forced green.
 
 == Known limitations (tracked, not silent)
 
-. *CI Agda version not exactly pinned.* CI installs Ubuntu's `agda`
-  (apt); local dev and the Nix flake differ (2.8.0 / flake-pinned).
-  The CI step *records and minimally asserts* the version (fails on a
-  wildly wrong major) so it is visible, not silently floating. Exact
-  parity via *CI-through-the-flake* is the tracked P1 follow-up — the
-  only honest way to pin Agda reproducibly.
+. *CI Agda exact pin* — *reproducible pin IMPLEMENTED 2026-05-18;
+  first-green verification delegated to CI.* `flake.nix` now pins, as
+  flake inputs: Agda via `nixpkgs nixos-24.11` (2.7.0.1), standard
+  library at tag `v2.3`, and `absolute-zero` at commit `3ff5cee…`
+  (previously nixpkgs-bundled stdlib + a local `absolute-zero`
+  checkout — neither reproducible). A hermetic `checks.suite`
+  (guardrail + four roots + N5 xfail) runs under that pinned
+  toolchain; an *additive* `flake-check` CI job (`nix flake check`)
+  exercises it. This is honest about its boundary: the dev
+  environment has no `nix`, so the flake was authored designed-correct
+  but its build is *first verified by CI*, not claimed green here. It
+  is `continue-on-error` until first green so a version delta
+  (2.7.0.1 vs the verified-green 2.8.0 / apt) is *surfaced*, not a
+  regression; the apt `check` + `cold-check` jobs remain the gate.
+  Open sub-item: on first green, flip `continue-on-error` to `false`
+  and retire the apt job; if red, the logged delta says which
+  nixpkgs/Agda to bump. (Cross-stack: a devShell-only `flake.nix`
+  also exists on the reframe stack PR #47; this one strictly
+  supersedes it.)
 . *External-fibre triangulation* — *DONE 2026-05-18*,
   `proofs/agda/EchoFiberTriangulation.agda` (wired into `All.agda`,
   pinned in `Smoke.agda`, `--safe --without-K`, zero postulates).
@@ -157,3 +170,12 @@ Pinned inputs: `standard-library` `v2.3`; `absolute-zero`
   follow-up entry is intentionally deferred to stack reconciliation
   (the append-only log evolves on the reframe/earn-back stack; adding
   a divergent entry on this `main`-based branch would fork it).
+* *2026-05-18 — CI-via-flake reproducible pin implemented.*
+  `flake.nix` evolved to pin Agda (nixpkgs nixos-24.11) + stdlib v2.3
+  + absolute-zero @3ff5cee as flake inputs, with a hermetic
+  `checks.suite`; additive `flake-check` CI job
+  (`continue-on-error`) added as the verifier. Authored without local
+  `nix` (none in dev env) — designed-correct, CI-verified, not
+  locally claimed green; flagged as such, gate unchanged. P1 item
+  status moved from "tracked follow-up" to "implemented, pending
+  first-green CI verification".
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..a9b3158
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,117 @@
+{
+  # SPDX-License-Identifier: PMPL-1.0-or-later
+  #
+  # Reproducible toolchain for echo-types — foundation P1 (CI-via-flake
+  # exact pin; docs/foundation.adoc §"Known limitations").
+  #
+  # CROSS-STACK NOTE. A simpler devShell-only flake.nix also exists on
+  # the reframe stack (commit 185eb74, PR #47). THIS file is a strict
+  # evolution of it (same devShell tools + PINNED Agda-library inputs +
+  # a hermetic `checks` output). At integration, this harden-stack
+  # version supersedes the reframe-stack one — no behavioural conflict,
+  # it only adds pins and checks.
+  #
+  # PINNING DECISION (explicit, surfaced — not assumed):
+  #   * Agda: nixpkgs `nixos-24.11` -> agda 2.7.0.1 (also ghc 9.6.6,
+  #     cabal 3.12.1.0, rustc 1.82.0, just 1.38.0 — .tool-versions
+  #     match). The verified-green local toolchain is agda 2.8.0; CI's
+  #     apt job runs yet another. The suite has so far proven robust
+  #     across apt-agda and 2.8.0; whether it also typechecks under
+  #     2.7.0.1 + stdlib v2.3 is VERIFIED BY the additive
+  #     `nix flake check` CI job, not assumed here. If that job is red
+  #     it surfaces the exact version delta to reconcile (bump the
+  #     nixpkgs input); the apt + cold-check jobs remain the gate
+  #     meanwhile, so nothing regresses.
+  #   * standard-library: PINNED to tag v2.3 as a flake input (was
+  #     nixpkgs-bundled — a different version than CI/local verify).
+  #   * absolute-zero: PINNED to commit 3ff5cee… as a flake input
+  #     (was a local ~/dev checkout — not reproducible / not CI-usable).
+  #
+  # NOTE: authored without a local `nix` (none in the dev env);
+  # flake.lock is generated and the build first verified BY CI.
+  # Designed-correct, CI-verified — not locally claimed green.
+  description = "echo-types reproducible toolchain (Agda + libs pinned)";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11";
+    agda-stdlib = {
+      url = "github:agda/agda-stdlib/v2.3";
+      flake = false;
+    };
+    absolute-zero = {
+      url = "github:hyperpolymath/absolute-zero/3ff5cee7f3fd002378089cd02f0c90a3747b45f0";
+      flake = false;
+    };
+  };
+
+  outputs = { self, nixpkgs, agda-stdlib, absolute-zero }:
+    let
+      systems = [ "x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin" ];
+      forAllSystems = nixpkgs.lib.genAttrs systems;
+
+      # The Agda libraries file as an exact store file — no heredoc,
+      # no Nix-string indentation hazard. Agda resolves each
+      # `.agda-lib`'s `include:` relative to that file's own directory,
+      # so pointing at the pinned inputs' own `.agda-lib` paths is
+      # sufficient. (Nix `"..."` interprets `\n` as a real newline.)
+      mkLibs = pkgs: pkgs.writeText "agda-libraries"
+        "${agda-stdlib}/standard-library.agda-lib\n${absolute-zero}/absolute-zero.agda-lib\n";
+    in {
+      devShells = forAllSystems (system:
+        let
+          pkgs = import nixpkgs { inherit system; };
+          libs = mkLibs pkgs;
+        in {
+          default = pkgs.mkShell {
+            name = "echo-types";
+            packages = [
+              pkgs.agda pkgs.just pkgs.ghc pkgs.cabal-install
+              pkgs.rustc pkgs.cargo pkgs.rustfmt pkgs.clippy
+            ];
+            shellHook = ''
+              export AGDA_DIR="$PWD/.agda"
+              mkdir -p "$AGDA_DIR"
+              cp -f ${libs} "$AGDA_DIR/libraries"
+              chmod u+w "$AGDA_DIR/libraries"
+              echo "echo-types devShell (PINNED):"
+              command -v agda >/dev/null && echo "  agda  : $(agda --version 2>/dev/null | head -n1)"
+              echo "  stdlib: v2.3 (flake input, pinned)"
+              echo "  absz  : 3ff5cee (flake input, pinned)"
+            '';
+          };
+        });
+
+      # Hermetic, reproducible verification: the flake-pinned Agda over
+      # the pinned stdlib v2.3 + absolute-zero, running the same
+      # guardrail + four roots + N5 expected-failure gate that CI's
+      # apt job runs. `nix flake check` exercises this.
+      checks = forAllSystems (system:
+        let
+          pkgs = import nixpkgs { inherit system; };
+          libs = mkLibs pkgs;
+        in {
+          suite = pkgs.runCommand "echo-types-suite"
+            { nativeBuildInputs = [ pkgs.agda pkgs.bash ]; }
+            ''
+              export HOME="$TMPDIR"
+              mkdir -p "$HOME/.agda"
+              cp -f ${libs} "$HOME/.agda/libraries"
+              # Agda needs a writable source tree (.agdai outputs).
+              cp -r ${self} src
+              chmod -R u+w src
+              cd src
+              bash tools/check-guardrails.sh proofs/agda
+              agda -i proofs/agda proofs/agda/All.agda
+              agda -i proofs/agda proofs/agda/Smoke.agda
+              agda -i proofs/agda proofs/agda/characteristic/All.agda
+              agda -i proofs/agda proofs/agda/examples/All.agda
+              if agda -i proofs/agda proofs/agda/characteristic/N5Falsifier.agda \
+                   > /dev/null 2>&1; then
+                echo "N5Falsifier unexpectedly typechecks — see foundation.adoc"
+                exit 1
+              fi
+              touch "$out"
+            '';
+        });
+    };
+}

From 8a24530741d229354d501fa26b9d9ffb8e4990e7 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 20 May 2026 15:07:47 +0100
Subject: [PATCH 2/3] =?UTF-8?q?echo-types:=20Pillar=20E=20=E2=80=94=20Back?=
 =?UTF-8?q?ground=20primer=20+=20Related=20work?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Clear two of the [EXPAND] tags on the establishment-track paper
against the canonical post-retraction structure:

* paper.adoc §Background and notation: self-contained primer for
  readers fluent in one of HoTT fibres / coeffect-graded-modality
  lineage but not both. Six subsections (type-theoretic setting,
  Σ-types and identity, HoTT fibres, coeffect/graded-modality
  lineage, thin-poset reindexing modalities, notation summary) plus
  an 18-row notation table whose every symbol is sourced from a real
  Agda module. Explicit on the post-retraction framing: Echo is the
  fibre; Echo is motivated by — not an instance of — the graded-comonad
  lineage; the load-bearing hypothesis is `≤g-prop`; there is no funext
  anywhere.

* paper.adoc §Related work: cherry-picked from a parallel agent's
  worktree, eight per-neighbour subsections (HoTT fibres,
  graded-comonad/coeffect/QTT lineage, lenses/optics, refinement
  types, setoid quotients, provenance semirings, IFC/modal type
  theories, synthesis), each with the (a) nearest construction,
  (b) what Echo adds, (c) what Echo does NOT add structure. All
  <<reframing-note>> cross-references resolve.

* types-abstract.adoc: added a per-neighbour related-work positioning
  block (6 bullets) mirroring the paper §Related work at abstract
  length. Abstract status remains "NOT submission-ready, pending
  re-review against reframed paper.adoc" — content alignment only,
  no submission-readiness change.

The Evaluation [EXPAND] and Ordinal consumer-evidence [EXPAND] tags
remain open (the latter is gated on the ordinal track hitting
Bachmann–Howard, firewalled per roadmap.md).

Build invariant unchanged: no Agda touched. Authority of every
"Echo does X" claim still backed by a verified module.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 docs/echo-types/paper.adoc          | 598 +++++++++++++++++++++++++++-
 docs/echo-types/types-abstract.adoc |  31 ++
 2 files changed, 611 insertions(+), 18 deletions(-)

diff --git a/docs/echo-types/paper.adoc b/docs/echo-types/paper.adoc
index 7559ca9..96e26dc 100644
--- a/docs/echo-types/paper.adoc
+++ b/docs/echo-types/paper.adoc
@@ -113,17 +113,237 @@ the rest of the paper bears.
   identity claims settled negatively and logged, including this
   development's own framing retraction (§7, <<reframing-note>>).
 
-== Background and notation [EXPAND]
+== Background and notation
+
+This section fixes vocabulary. A reader fluent in dependent type
+theory may not be equally fluent in *both* HoTT fibres and the
+coeffect / graded-modality lineage, and the rest of the paper assumes
+both at the level of recognition rather than internalisation. We aim
+the exposition at exactly that reader: pin the symbols, recall the
+two prior-work neighbourhoods the development sits between, and state
+what `--safe --without-K` does and does not give us. There are no new
+claims here.
+
+=== Type-theoretic setting
+
+The development is Agda + agda-stdlib 2.3 under `--safe --without-K`
+with zero postulates and no escape pragmas. Concretely this excludes:
+Streicher's axiom K (so we may not assume UIP on arbitrary types);
+univalence and any other postulated equivalence; function
+extensionality (`funext`); the law of excluded middle; choice; and
+proof-irrelevance pragmas. The only propositional equality we have is
+Martin-Löf's inductive identity type `_≡_` with its single
+constructor `refl`, and the only dependent pair we have is `Σ`.
+
+The funext-relativity of §3 is *not* a quarantine: there is no funext
+module anywhere in the development, no postulated equality of
+functions, no isolated `Transport.agda`-style escape. The genuine
+funext dependence is *internal* — it sits in the gap between
+pointwise agreement `∀ v → m' v ≡ m v` and morphism equality
+`m' ≡ m`. The 2026-05-18 reframing (`docs/retractions.adoc`,
+<<reframing-note>>) closed an earlier mis-framing of this dependence
+as a quarantined module. The earn-back (Gate F4,
+`EchoPullbackUnivF4.agda`) takes the funext dependence
+*compositionally* via an explicit module parameter `FunExt₀` — never
+a postulate, never a hidden hypothesis. The trusted base is
+unchanged.
+
+=== Σ-types and the identity type
+
+`Σ A (λ x → P x)` is the standard dependent pair: a value of `A` and
+a value of `P x`. We write `Σ A P` when `P` is already a function and
+`(x , p)` for pair construction. Echo is a Σ-type at a specific shape:
+
+[source,agda]
+----
+Echo : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → B → Set (a ⊔ b)
+Echo {A = A} f y = Σ A (λ x → f x ≡ y)
+----
+
+A witness `(x , p) : Echo f y` is a *source* `x : A` together with
+the propositional equality `p : f x ≡ y` certifying that `x` lands at
+`y` under `f`. The identity type `_≡_` is the standard Martin-Löf
+inductive one; `refl` is its sole constructor. Equational reasoning
+uses stdlib's `≡-Reasoning` block syntax (`begin … ≡⟨ … ⟩ … ∎`).
+Bijections are stdlib `Function.Bundles._↔_`, constructed via
+`mk↔ₛ′`. We never use propositional truncation `‖ A ‖` (it would
+collapse the witness data this development exists to keep);
+truncation is named as a contrast in §"Related work" but does not
+appear in any verified statement.
+
+=== HoTT fibres
+
+The homotopy fibre of `f : A → B` at `y : B` (HoTT Book Def. 4.2.4)
+is `fib f y := Σ A (λ x → f x ≡ y)`. This is *definitionally* `Echo
+f y` under a renaming of the function symbol; Pillar A
+(`EchoFiberBridge.agda`) discharges the bridge `echo↔fib : Echo f y
+↔ fiber f y` as `refl` round-trips. We say "homotopy fibre" and
+"Echo" interchangeably; the paper's terminological choice is to use
+"Echo" for the loss-tracking reading and "fibre" when contrasting
+with the broader HoTT framework. There is no difference of
+construction.
+
+Two stylistic notes for HoTT readers. (1) We do *not* use cubical
+Agda, univalence, or HITs anywhere. Every statement is in
+intensional MLTT + Σ + `_≡_`. (2) The fibre is *not* propositionally
+truncated. The whole development depends on the witness `x` being
+proof-relevant: `echo-true ≢ echo-false`
+(`EchoCharacteristic.agda`) and the family of `echo-not-prop`
+exhibits in `proofs/agda/examples/{TropicalArgmin, EpistemicUpdate,
+LinearErasure}.agda` certify the loss of structure under truncation.
+The "structured loss" reading is exactly this: a target value `y :
+B` underdetermines its source, and the (untruncated) fibre records
+*which* source was actually used along with the equation that
+justifies it.
+
+=== Coeffect / graded-modality lineage
+
+The vocabulary the paper uses for "loss-graded" comes from the
+coeffect and graded-modality tradition: Petriček, Orchard and
+Mycroft (ICFP 2014) on coeffects as a calculus of context-dependent
+computation; Brunel, Gaboardi, Mazza and Zdancewic (ESOP 2014) on
+a core quantitative coeffect calculus; Atkey (LICS 2018) on the
+syntax and semantics of Quantitative Type Theory; Orchard, Liepelt
+and Eades (ICFP 2019) on Granule's graded modal types; and at the
+comonad side, Uustalu and Vene's classical comonadic notions of
+computation (ENTCS 2008) which the graded-comonad refinement
+specialises. The shared shape across these works is a family `D_r`
+of types indexed by elements of a (pre)ordered *grade* structure
+with semiring or join-semilattice algebra, equipped with a counit
+`D_0 X → X` and (in the graded-comonadic case) a comultiplication
+`D_{r·s} X → D_r (D_s X)`. The laws are the graded analogues of
+the comonad triangle and pentagon.
+
+The previous draft of this paper presented Echo as an instance of
+this lineage. That framing was retracted (<<reframing-note>>) for a
+concrete and verifiable reason: `EchoGradedComonad.agda` exhibits no
+nested family `GEcho (GEcho …)` and no structure map of shape
+`D_{g₁ ⊔ g₂} ⇒ D_{g₁} D_{g₂}`. What is mechanised is the strictly
+smaller thin-poset reindexing modality described next; this is the
+lineage Echo is *motivated by* and not the structure Echo
+*instantiates*.
+
+=== Thin-poset reindexing modalities
+
+The structure Echo actually carries is a monotone family `GEcho`
+over a join-semilattice `(Grade, ⊔, keep)` of loss grades, together
+with a functorial reindexing action `degrade : g₁ ≤g g₂ → GEcho g₁
+→ GEcho g₂`. Three properties make this useful and pin its load:
+
+* The order `_≤g_` is *propositional* (`≤g-prop`): there is at most
+  one inhabitant of `g₁ ≤g g₂` for any given pair. This is the
+  paper's single load-bearing hypothesis (§5 measures content
+  *exactly* at this hypothesis).
+* `degrade` is *functorial* (`degrade-compose`): composing two
+  degradations through a common intermediate agrees with degrading
+  directly.
+* The join `⊔` has the usual universal property
+  (`≤g-⊔-{left,right,univ}`), making `keep` the bottom and joins the
+  least common upper bounds.
+
+The three coherence equations the paper names
+(`gcomonad-counit-{l,r}`, `gcomonad-coassoc`, retained for module
+continuity) all collapse to `degrade-compose` + `≤g-prop` in the
+common-upper-bound idiom (§4). They are not evidence of a coherence
+tower; they are evidence that thinness already discharges everything
+the names appear to demand. This is the calibration result the paper
+contributes.
+
+=== Notation summary
+
+The notation pinned to specific modules:
+
+[cols="1,2,2", options="header"]
+|===
+| Symbol | Meaning | Source
+
+| `Σ A P`, `(x , p)`
+| Dependent pair, pair construction
+| stdlib `Data.Product`
+
+| `_≡_`, `refl`
+| Propositional equality, its constructor
+| stdlib `Relation.Binary.PropositionalEquality`
+
+| `_↔_`, `mk↔ₛ′`
+| Bijection bundle, its smart constructor
+| stdlib `Function.Bundles`
+
+| `Σ-≡,≡→≡`
+| Pair-equality from component equalities (UIP-free)
+| stdlib `Data.Product.Properties`
+
+| `Echo f y`
+| `Σ A (λ x → f x ≡ y)` — fibre at `y`
+| `proofs/agda/Echo.agda`
+
+| `fib f y`, `fiber f y`
+| Homotopy fibre; same as `Echo f y`
+| `EchoFiberBridge.agda`
+
+| `echo↔fib`
+| Bridge `Echo f y ↔ fiber f y` (`refl` round-trips)
+| `EchoFiberBridge.agda`
+
+| `map-over`, `map-square`
+| Action of morphisms / commuting squares on fibres
+| `Echo.agda`
+
+| `Grade`, `keep`
+| Loss-grade carrier; bottom (no loss)
+| `EchoGraded.agda`
 
-Σ-types, the identity type, homotopy fibres, graded/coeffect
-comonads, the join-semilattice of loss grades. Agda `--safe
---without-K` and what it excludes (K, univalence, funext).
+| `_≤g_`, `≤g-prop`
+| Loss-grade order; its propositionality
+| `EchoGraded.agda`
 
-NOTE: *[EXPAND]* — flesh out with a self-contained primer on graded
-comonads (Petriček–Orchard–Mycroft; Brunel et al.; Atkey QTT;
-Orchard–Liepelt–Eades / Granule) and a one-paragraph HoTT-fibre
-recap, so the paper is readable by both the QTT and the HoTT
-communities without external lookup.
+| `_⊔g_`, `≤g-⊔-{left,right,univ}`
+| Join; its universal property
+| `EchoGraded.agda`
+
+| `GEcho g`, `degrade`
+| Loss-graded family; reindexing action
+| `EchoGraded.agda`
+
+| `degrade-compose`
+| Functoriality of `degrade`
+| `EchoGraded.agda`
+
+| `gextract`, `gduplicate`
+| Retained names; identity coercion and join-left reindex
+| `EchoGradedComonad.agda`
+
+| `gcomonad-counit-{l,r}`, `gcomonad-coassoc`
+| Three coherence equations; collapse to `degrade-compose`+`≤g-prop`
+| `EchoGradedComonad.agda`
+
+| `GradedLossModel`, `⊑-prop`
+| Carrier-parametric model interface; load-bearing field
+| `EchoRelModel.agda`
+
+| `GCLaws`
+| Coherence equations proved once, parametric in the carrier
+| `EchoRelModel.agda`
+
+| `FunExt₀`
+| Module parameter for the conditional terminality earn-back
+| `EchoPullbackUnivF4.agda`
+|===
+
+Conventions: universe levels are usually elided (write `Set` for
+`Set a` etc.) when there is no ambiguity. `(x , p)` always
+right-associates: `(x , y , p)` is `(x , (y , p))`. We use Agda's
+mixfix syntax throughout, including `_⊔_` for joins; the
+disambiguation rule is that `⊔` over types is universe-level join
+and `⊔g` over grades is the loss-grade join. Where a stdlib symbol
+collides with a development-local one, we qualify
+(`EchoGraded.degrade`, `Echo.map-over`).
+
+// TODO(bibliography): bib entries needed when a venue/template is
+// chosen: HoTT Book (Def. 4.2.4); Petriček, Orchard and Mycroft
+// (ICFP 2014); Brunel et al. (ESOP 2014); Atkey (LICS 2018);
+// Orchard, Liepelt and Eades (ICFP 2019, Granule); Uustalu and Vene
+// (ENTCS 2008); Gaboardi et al. (ICFP 2016).
 
 == The pullback presentation and its pointwise mediator property
 
@@ -333,15 +553,357 @@ thinness-only content) stated as honest bounds, *not* spun as
 strengths; threats to validity, including the Gate-2 audit's own
 "single recipe" finding.
 
-== Related work [EXPAND]
-
-NOTE: *[EXPAND]* — detailed positioning against: Granule / QTT graded
-modalities; comonadic notions of computation (Uustalu–Vene);
-coeffects (Petriček–Orchard–Mycroft); HoTT fibrewise constructions;
-lens / optic literature (the witness-transport leg of
-`echo-pullback-univ` resembles the very-well-behaved-lens laws). Make
-the novelty crisp: not a new object, but a fully mechanised
-characterisation package with a falsifiable-gate methodology.
+== Related work
+
+This section positions Echo against its nearest neighbours.  The
+honest summary is that Echo introduces *no new object*: it is the
+homotopy fibre, dressed with a thin-poset reindexing action, packaged
+under a falsifiable-gate methodology.  Per neighbour, we name (a) the
+nearest existing construction, (b) what the verified Agda adds over
+that construction, and (c) — equally important — what it does *not*
+add.  The repository's adjacency notes
+(`docs/adjacency/{quotients,galois-connections,refinement-types,information-flow,provenance,modal-type-theories,hott-fibers,lenses-and-optics,setoid-quotients,provenance-semirings}.adoc`)
+contain the per-neighbour distinctness arguments at gate-1
+granularity; here we draw out the positioning specifically relevant
+to the *characterisation package* (Pillars A–D) rather than to
+gate-1's bare-construction distinctness.
+
+=== HoTT homotopy fibres
+
+The nearest construction is the homotopy fibre `fib f y` (HoTT Book
+Def. 4.2.4).  `Echo f y` is the homotopy fibre.  Pillar A
+(`proofs/agda/EchoFiberBridge.agda`) discharges this as a
+`refl`-round-tripping bridge `echo↔fib : Echo f y ↔ fiber f y`; the
+"bridge" is the identity, as it must be.  This is the most-coincident
+neighbour in the entire literature, and we own the coincidence loudly
+(see <<reframing-note>> and §1).  A category theorist or HoTT user
+should recognise the construction on first sight.
+
+What Echo adds *over the bare fibre* is not a new object but an
+organising vocabulary plus four verified deliverables that HoTT users
+typically do not unify:
+
+* a funext-relative pointwise mediator property
+  (`echo-pullback-univ` in `EchoPullback.agda`; conditionally
+  strengthened to genuine terminality under an explicit `funext`
+  module parameter in `EchoPullbackUnivF4.agda`);
+* a thin-poset reindexing action on a loss-grade lattice
+  (`EchoGradedComonad.agda`'s three coherence equations, each
+  collapsing to `degrade-compose` + `≤g-prop`);
+* a separating model that *measures* the modality's content over
+  generic Σ at exactly `≤g-prop` (`EchoSeparating.agda`);
+* a postulate-free build (`--safe --without-K`, no escape pragmas,
+  CI-enforced) so that the whole package is evidence for
+  conservativity over MLTT+Σ.
+
+What Echo does *not* add over HoTT: anything foundational.  A
+cubical-Agda user has access to univalence and HITs and can express
+every construction here natively, frequently more cleanly.  The
+contribution is at the *exposition* and *packaging* level — naming
+the thin-poset reindexing modality, isolating its load-bearing
+hypothesis, and shipping it under a retraction discipline — not at
+the foundations level.
+
+What we explicitly do *not* claim is distinctness from the homotopy
+fibre.  The win lives one step to the side: against
+*propositionally-truncated* fibres, where `‖ Echo f y ‖` discards the
+witness-type data, the un-truncated form retains it
+(`echo-not-prop`-shaped certificates in
+`proofs/agda/examples/{TropicalArgmin,EpistemicUpdate,LinearErasure}.agda`).
+This is the same shape of argument as against refinement types and
+relational information-flow, restated in the modality the HoTT
+framework provides for it.
+
+=== Graded comonads, coeffects, and QTT (the lineage we are motivated
+by, but explicitly not an instance of)
+
+The graded-comonadic lineage runs through Uustalu–Vene's comonadic
+notions of computation; Petriček–Orchard–Mycroft coeffects;
+Brunel–Gaboardi–Mazza–Zdancewic graded modal types; Katsumata's
+parametric effect monads (mirrored at the comonad side); Atkey's
+Quantitative Type Theory; and Orchard–Liepelt–Eades' Granule.  The
+shared idea is a family `D_r` indexed by elements of a (pre)ordered
+*grade* structure with semiring or join-semilattice algebra,
+equipped with a counit `D_0 X → X` and a comultiplication
+`D_{r·s} X → D_r (D_s X)`; the laws are the graded analogues of the
+usual comonad triangle and pentagon.
+
+The development presented here was originally framed as an instance
+of this lineage and was retracted from that framing in adversarial
+review (see <<reframing-note>>).  Stating the corrected position
+plainly: `EchoGradedComonad.agda` does *not* exhibit a graded
+comonad.  There is no nested family `GEcho (GEcho …)` and no
+structure map of shape `D_{g₁ ⊔ g₂} ⇒ D_{g₁} D_{g₂}` anywhere in the
+codebase.  What is mechanised is a *single* grade application
+`gduplicate g₁ g₂ : GEcho g₁ → GEcho (g₁ ⊔ g₂)` — the join-left
+reindex `degrade (≤-⊔-left g₁ g₂)`.  The three coherence equations
+(`gcomonad-counit-{l,r}`, `gcomonad-coassoc`) hold for one reason:
+the grade order is thin (`≤g-prop`) and `degrade` is functorial
+(`degrade-compose`).  We retain the names `gextract` /
+`gduplicate` for module-continuity reasons, with §4 stating plainly
+what they are.
+
+What Echo *is*, against this lineage, is a *loss-graded reindexing
+modality* — a thin-poset action with a functorial monotone
+reindex.  This sits one rung *below* a graded comonad in the
+ladder of structure: every graded comonad over a thin grade poset
+collapses to one of these, but not conversely.  Against QTT
+specifically, the `LinearErasure` example in
+`proofs/agda/examples/LinearErasure.agda` and the linearity-side
+analogue in `EchoLinear.agda` (two-mode `linear ⊑ affine`
+decoration, `degradeMode`, `degradeMode-compose`,
+`degradeMode-via-join`) exhibit the recipe at the same shape that
+QTT's `0 ≤ 1 ≤ ω` quantity ordering carries.  On *bare echo*, QTT
+and Echo coincide: the inverse problem "given erased term at
+quantity ν, what was the source annotation?" is natively
+`Σ (q : Quantity) (erase q ≡ y)`, which is `Echo erase y`.
+
+What Echo adds over the graded-comonad lineage: nothing
+load-bearing on judgmental grounds — Echo introduces no new
+formation rule, context structure, or substructural discipline (§1
+"Why not 'linear or dependent'").  What is added is a verified
+*calibration result*: the separating model (§5) pins down the
+single load-bearing hypothesis (`≤g-prop`) and confirms that
+generic Σ-functoriality survives without it.  This is the kind of
+result the graded-modality literature typically does not ship at
+this granularity, but the result *is itself* about how little
+content the modality adds over generic Σ.  We report it as
+calibration, not as evidence of a rich coherence tower (§4.2).
+
+What Echo does *not* add over QTT / Granule: any judgmental
+extension, any quantity-sensitive elimination rule, any syntactic
+modal account at the term language.  A QTT encoding of the recipe
+appears feasible (see `docs/adjacency/modal-type-theories.adoc`'s
+recipe-level open question); whether QTT carries
+`RoleGraded.choreo-grade-commute` natively without echo machinery is
+a genuinely open question this paper does not close.
+
+=== Lenses and optics (the witness-transport leg)
+
+The nearest construction is a lawful lens `get : S → A`,
+`put : S → A → S` with the three lens laws, generalising through
+prisms, traversals, and the van Laarhoven / profunctor / indexed
+optics families.  Optics are the dominant engineering vocabulary
+for "structured access to a part of a larger whole".  The
+witness-transport leg of `echo-pullback-univ` — the cone-morphism
+notion carrying a `coherent : ∀ v → f (factor v) ≡ y` field,
+transported by `map-over` (`proofs/agda/Echo.agda`) and `map-square`
+along a commuting square — is in the optic neighbourhood; in
+particular, `map-square` is structurally adjacent to the
+2-cell composition of optics.
+
+What Echo adds over lenses (catalogued more fully in
+`docs/adjacency/lenses-and-optics.adoc`):
+
+* *Explicit source-retention instead of set-back.*  Echo records
+  a specific source alongside the equation `f x ≡ y`; lenses
+  reconstruct an updated source from an existing one through `put`.
+  The witness `(true , false) : Echo visible true` is a retained
+  state, not the machinery for overwriting one.
+* *Honest asymmetry on the put side.*  `no-section-visible` in
+  `EchoCharacteristic.agda` proves there is no section
+  `Bool → Bool × Bool` of `visible`; the echo framing is honest
+  about one-argument impossibility and captures what is
+  nevertheless retained.
+* *Sequential composition as an isomorphism theorem.*
+  `Echo-comp-iso : Echo (g ∘ f) y ↔ Σ B (λ b → Echo f b × g b ≡ y)`
+  (Echo.agda) ships sequential composition as a verified
+  equivalence with both round-trips, plus pentagon coherence
+  (`Echo-comp-iso-pent-{B, echo}`) and a cancellation iso
+  (`cancel-iso`) when the outer leg is invertible.  The optic
+  analogues ship as definitions.
+* *Residue as first-class lowering.*  `EchoResidue.echo-to-residue`
+  lowers a full echo to a certificate; `no-section-collapse-to-residue`
+  witnesses strict non-recoverability.  Optics do not typically
+  ship a quotient-of-witness with a non-recoverability proof.
+
+What Echo does *not* add over lenses: no update / `put`, no
+round-trip laws, no profunctor or van Laarhoven encoding, no
+effectful / indexed / monadic / affine optic.  Optics are
+designed around reversible access; echo around witness
+retention under non-reversibility.  The two coincide at the
+get-side skeleton and diverge on the put / residue question.
+
+=== Refinement types
+
+Two implementation traditions need to be distinguished.  In
+*Σ-relevant refinement* (Agda, Coq, dependently-typed ML), the
+refinement type `{ x : A | P x }` literally *is* `Σ A P`; with
+`P x := f x ≡ y`, this is `Echo f y`.  **No win for echo on the
+type level.**  In *propositional-predicate refinement* (F\*,
+Liquid Haskell, SMT-backed systems), the predicate is a
+proposition and the refinement type is the propositional
+truncation of `Σ A P`, discarding individual witness identity.
+Here `echo-not-prop` (gate-3 exhibits at
+`proofs/agda/examples/{TropicalArgmin,EpistemicUpdate,LinearErasure}.agda`)
+is the formal certificate that the truncation loses what Echo
+retains.
+
+The narrow claim is *stronger* than the overstated one: against
+Σ-relevant refinement Echo is the same construction with
+different surface syntax (and the characterisation package
+applies verbatim to that surface); against propositional
+refinement, the truncation argument lands formally on three
+domains.
+
+=== Setoid quotients
+
+A setoid `(A, ~)` handles equivalence extrinsically: functions
+must respect `~` and equality up to `~` is proved.  The echo
+pattern "same visible output, distinct retained source" can be
+read as "quotient by the kernel of `f`".  Echo's kernel is
+*implicit* — named through the function `f` rather than through
+a separate relation — and *proof-relevant*: `echo-true ≢ echo-false`
+in `EchoCharacteristic.agda` exhibits distinct representatives
+that a setoid reader would identify.  The graded hierarchy
+(`EchoGraded.degrade`, `degrade-compose`, `degrade-via-join`)
+collapses what a setoid presentation would express as one
+relation per grade plus respect proofs into a single function
+family indexed by `g₁ ≤g g₂`, with composition pinned by `refl`.
+
+Echo does *not* add quotient types (intensional Agda cannot form
+them; the development does not attempt it), nor a quotient
+elimination principle.  A setoid partisan can read the
+development as "pointed setoid with remembered representative",
+under which the residue hierarchy is "retain, then forget; note
+you cannot un-forget" — true and not deep.  The reply is that
+the family `Echo f` is functorial under `map-over` /
+`map-square` without invoking setoid-respecting maps, and that
+the bridges (graded, linear, choreographic, epistemic, tropical)
+integrate as a single recipe rather than as separate quotients.
+
+=== Provenance and provenance semirings
+
+K-provenance (Green–Karvounarakis–Tannen) annotates database
+tuples by elements of a commutative semiring `K`, with
+relational-algebra operations composing annotations via
+`+, ·, 0, 1`; specialisations include boolean, bag, why/where,
+and free polynomial provenance.  The shared motive with Echo is
+*tracking what survives under lossy operations*; the mechanism
+is different.  Echo attaches a *proof term* `(x , p)` where
+`p : f x ≡ y`, not a semiring element; `EchoIndexed.Echoᵢ`
+extends the witness by a role index so the same visible output
+can carry different provenance certificates for different
+observers; `EchoGraded.degrade-compose` /
+`degrade-via-join` show any two factorings of a degradation
+through the order agree on the underlying echo — a thin-poset
+coherence, not a semiring homomorphism.
+
+Echo does *not* ship a semiring, a relational-algebra reading,
+free polynomial provenance, or query-equivalence theorems.  A
+provenance researcher can read the residue hierarchy
+(`keep`, `residue`, `forget`) as K-provenance for an
+impoverished `K`; the non-trivial replies are (i) the witnesses
+are types, not semiring elements, so `Echo collapse tt` retains
+two inhabitants no annotation algebra can distinguish, and (ii)
+the bridges (linear, choreographic, epistemic) are not
+naturally semiring structures.
+
+The single-witness vs propositional-truncation framing is
+sharper than refinement-types' bare truncation argument for
+this neighbour: provenance specifically tracks *one* source per
+output rather than truncating to "some source exists", and
+`echo-not-prop` is the formal certificate at the same shape.
+
+=== Information-flow non-interference and modal type theories
+
+Goguen–Meseguer style non-interference is propositional /
+relational about indistinguishability; gate-3's
+`EpistemicUpdate` example formalises the truncation win at the
+shape "multiple consistent worlds, truncation loses individual
+world identity, breaking `refine-injective`".  Against
+type-theoretic IFC variants (e.g., the dependently-typed
+information-flow tradition) the recipe-level question is open;
+no dedicated `proofs/agda/adjacency/IFC.agda` formalisation
+exists.
+
+Modal type theories (QTT, Reed–Pfenning judgmental S4, adjoint
+modalities, cohesive type theory) are the most under-formalised
+adjacency case.  Against propositional-mode accounts the
+truncation argument lands via `LinearErasure.echo-not-prop`.
+Against modal type theories with sufficient ambient mode
+structure, *Echo coincides with the native modal Σ-construction
+on bare echo*; whether the coincidence extends to the
+characterisation package — and specifically whether QTT
+expresses the thin-poset reindexing modality natively without
+echo machinery — is a recipe-level open question
+(`docs/adjacency/modal-type-theories.adoc`, retraction
+condition 1).  Stating the coincidence plainly is more honest
+than overstating distinctness.
+
+=== Synthesis: a characterisation package, not a new object
+
+The cross-cutting claim is not that Echo is a new construction.
+It is the homotopy fibre.  What this paper contributes is a
+*fully mechanised characterisation package* for that construction
+together with the smallest interesting modality over it:
+
+. a definitional Σ-identity bridge to the HoTT fibre (Pillar A);
+. a funext-relative pointwise mediator property at the pullback
+  presentation, with strict terminality earned back under an
+  explicit `funext` module parameter (Pillar B-1, §3);
+. a loss-graded reindexing modality whose three coherence
+  equations provably reduce to thinness of the grade order
+  (Pillar B-2, §4);
+. a separating model that locates that reduction exactly
+  (Pillar C, §5);
+. a carrier-parametric abstraction over a fixed grade poset
+  (Pillar D, §6);
+. a postulate-free `--safe --without-K` build with zero escape
+  pragmas (§6.2);
+. a falsifiable-gate methodology with a public retraction log
+  (`docs/retractions.adoc`, §7), of which the 2026-05-18
+  reframing is itself the working example.
+
+The novelty is in the *packaging discipline*, not in the
+underlying object.  Against each adjacent framework we are
+honest about what Echo *does not* add: foundations vs HoTT,
+judgmental extensions vs the graded-modality lineage, update
+machinery vs lenses, surface algebra vs provenance semirings,
+quotient types vs setoid quotients, recipe-level distinctness
+against modal type theories with sufficient ambient structure.
+The standing we claim is exactly that of a characterisation
+package whose load-bearing hypothesis (`≤g-prop`) is isolated,
+whose models are pinned, and whose bounds are stated rather
+than spun.
+
+NOTE: *Bib TODO.*  Inline (Name Year) references in this
+section that require formal bibliography entries when a venue
+template is chosen:
+HoTT Book (Univalent Foundations Program 2013, §§3.7, 4.2);
+Vezzosi–Mörtberg–Abel "Cubical Agda" (ICFP 2019);
+Uustalu–Vene "Comonadic notions of computation" (ENTCS 2008);
+Petriček–Orchard–Mycroft "Coeffects: a calculus of context-dependent
+computation" (ICFP 2014);
+Brunel–Gaboardi–Mazza–Zdancewic "A core quantitative coeffect
+calculus" (ESOP 2014);
+Katsumata "Parametric effect monads and semantics of effect
+systems" (POPL 2014);
+Atkey "Syntax and semantics of quantitative type theory"
+(LICS 2018);
+Orchard–Liepelt–Eades "Quantitative program reasoning with graded
+modal types" (ICFP 2019, Granule);
+Reed "A judgmental deconstruction of modal logic" (CMU TR 2009);
+Pfenning–Davies "A judgmental reconstruction of modal logic"
+(MSCS 2001);
+Birkedal–Møgelberg–Schwinghammer–Støvring "First steps in
+synthetic guarded domain theory" (LICS 2011);
+Shulman "Brouwer's fixed-point theorem in real-cohesive homotopy
+type theory" (2017);
+Foster–Greenwald–Moore–Pierce–Schmitt "Combinators for
+bidirectional tree transformations: a linguistic approach to the
+view-update problem" (POPL 2005, lenses);
+Pickering–Gibbons–Wu "Profunctor optics: modular data
+accessors" (Art Sci. Eng. Program. 2017);
+Cousot–Cousot "Abstract interpretation: a unified lattice
+model" (POPL 1977);
+Goguen–Meseguer "Security policies and security models"
+(IEEE S\&P 1982);
+Green–Karvounarakis–Tannen "Provenance semirings" (PODS 2007);
+Swamy et al. "Dependent types and multi-monadic effects in F\*"
+(POPL 2016);
+Vazou–Seidel–Jhala–Vytiniotis–Peyton Jones "Refinement types for
+Haskell" (ICFP 2014, Liquid Haskell).
 
 [#reframing-note]
 == Reframing note (2026-05-18)
diff --git a/docs/echo-types/types-abstract.adoc b/docs/echo-types/types-abstract.adoc
index 3bb376f..820073e 100644
--- a/docs/echo-types/types-abstract.adoc
+++ b/docs/echo-types/types-abstract.adoc
@@ -139,6 +139,37 @@ that locates that reduction, a carrier-parametric abstraction, and a
 postulate-free build, all under a falsifiable-gate methodology that
 has been exercised on this development's own claims.
 
+Positioning by neighbour (full per-neighbour analysis in `paper.adoc`
+§"Related work"):
+
+* *HoTT fibres.* Echo *is* the fibre (`echo↔fib`, `refl` round-trips).
+  The win is not against HoTT but one step to the side: against
+  *propositionally-truncated* fibres, where `‖ Echo f y ‖` discards
+  witness identity, the un-truncated form retains it
+  (`echo-not-prop` certificates).
+* *Graded comonads / coeffects / QTT* (Uustalu–Vene; Petriček et al.;
+  Brunel et al.; Atkey; Granule). Echo is *motivated by* this lineage
+  but explicitly *not* an instance — `EchoGradedComonad.agda` exhibits
+  no nested `D_r D_s`. What we provide is a *calibration*: the
+  separating model isolates the single load-bearing hypothesis
+  (`≤g-prop`) at which generic Σ-functoriality stops being enough.
+* *Lenses / optics.* The witness-transport leg of `map-over` /
+  `map-square` is in the optic neighbourhood; Echo adds explicit
+  source-retention and honest one-sided non-recoverability (`no-section-*`),
+  but ships no `put`, no van Laarhoven encoding.
+* *Refinement types.* Σ-relevant refinement (Agda/Coq) coincides with
+  Echo definitionally; propositional-predicate refinement (F\*, Liquid
+  Haskell) loses what Echo retains (truncation argument).
+* *Setoid quotients / provenance semirings.* Echo's kernel is implicit
+  (named through `f`) and proof-relevant; it ships no quotient
+  elimination and no semiring. Provenance researchers can read the
+  residue hierarchy (`keep`/`residue`/`forget`) as K-provenance for an
+  impoverished `K`.
+* *Modal type theories.* The recipe-level question — whether QTT or
+  Reed–Pfenning S4 expresses the thin-poset reindexing modality
+  natively without echo machinery — is genuinely open and explicitly
+  not closed here.
+
 == Author / artefact statement
 
 Mechanised in Agda (stdlib 2.3), `--safe --without-K`, no postulates.

From 2e787611486eb65d3149ef1b8d10abd0519d569b Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 20 May 2026 15:08:17 +0100
Subject: [PATCH 3/3] licence: collapse PMPL SPDX identifier to MPL-2.0 (owner
 direction 2026-05-20)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Owner direction (2026-05-20) supersedes the prior PMPL-1.0-or-later
estate policy: the *stated* licence (SPDX-License-Identifier,
LICENSE file, README badge) becomes MPL-2.0; the PMPL framing is
preserved as a narrative/cultural overlay in docs/PMPL-NARRATIVE.adoc,
not as a separate SPDX identifier or legal text.

No legal effect change: MPL-2.0 was already the lawyer-confirmed
operative legal effect of PMPL-1.0-or-later. What is dropped is the
foreign SPDX identifier that registries / scanners / downstream
tooling treated as non-standard.

Changes:
* 29 source/config/workflow files: SPDX header
  PMPL-1.0-or-later/PMPL-1.0 → MPL-2.0 (.a2ml, .adoc, .yml,
  Containerfile, .nix, shell scripts, .editorconfig, .envrc).
* README.md: licence badge → MPL-2.0 (https://www.mozilla.org/en-US/MPL/2.0/).
* stapeln.toml + arghda-core/Cargo.toml: `license = "MPL-2.0"`.
* scripts/kernel-guard.sh + .github/workflows/agda.yml: removed
  the now-stale "MPL-2.0 is the legal fallback until PMPL is
  formally recognised" comment.
* .machine_readable/6a2/STATE.a2ml: license field → MPL-2.0.
* .machine_readable/6a2/ECOSYSTEM.a2ml: convention block re-worded
  to point at docs/PMPL-NARRATIVE.adoc as the narrative location.
* contractiles/Trustfile.a2ml: LICENSE-check trust grep now looks
  for "Mozilla Public License" instead of the prior PMPL pattern.
* docs/PMPL-NARRATIVE.adoc (new): records what the Palimpsest
  framing contributed (multi-author/palimpsest reading,
  source-availability discipline, narrative coherence over
  registry convenience), the working-discipline commitments that
  survive MPL-2.0, what is no longer claimed, the going-forward
  header convention, and the history.

LICENSE and LICENSE-docs files unchanged: they were already
MPL-2.0 / CC-BY-4.0 respectively (no PMPL text to migrate).

Intentional remaining PMPL strings: docs/PMPL-NARRATIVE.adoc
(the narrative itself) and the one pointer to it in ECOSYSTEM.a2ml.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 .editorconfig                              |   2 +-
 .envrc                                     |   2 +-
 .github/workflows/agda.yml                 |   3 +-
 .github/workflows/governance.yml           |   2 +-
 .github/workflows/hypatia-scan.yml         |   2 +-
 .github/workflows/mirror.yml               |   2 +-
 .github/workflows/scorecard.yml            |   2 +-
 .machine_readable/6a2/AGENTIC.a2ml         |   2 +-
 .machine_readable/6a2/ECOSYSTEM.a2ml       |  11 ++-
 .machine_readable/6a2/META.a2ml            |   2 +-
 .machine_readable/6a2/NEUROSYM.a2ml        |   2 +-
 .machine_readable/6a2/PLAYBOOK.a2ml        |   2 +-
 .machine_readable/6a2/STATE.a2ml           |   4 +-
 0-AI-MANIFEST.a2ml                         |   2 +-
 Containerfile                              |   2 +-
 EXPLAINME.adoc                             |   2 +-
 QUICKSTART-DEV.adoc                        |   2 +-
 QUICKSTART-MAINTAINER.adoc                 |   2 +-
 QUICKSTART-USER.adoc                       |   2 +-
 README.md                                  |   4 +-
 TOPOLOGY.adoc                              |   2 +-
 arghda-core/Cargo.toml                     |   2 +-
 contractiles/Dustfile.a2ml                 |   2 +-
 contractiles/Intentfile.a2ml               |   2 +-
 contractiles/Mustfile.a2ml                 |   2 +-
 contractiles/Trustfile.a2ml                |   4 +-
 docs/PMPL-NARRATIVE.adoc                   | 106 +++++++++++++++++++++
 docs/echidna-design-search-2026-04-28.adoc |   2 +-
 docs/echo-types/MAP.adoc                   |   2 +-
 docs/echo-types/echo-kernel-note.adoc      |   2 +-
 flake.nix                                  |   2 +-
 scripts/kernel-guard.sh                    |   3 +-
 stapeln.toml                               |   4 +-
 tools/check-guardrails.sh                  |   2 +-
 34 files changed, 148 insertions(+), 43 deletions(-)
 create mode 100644 docs/PMPL-NARRATIVE.adoc

diff --git a/.editorconfig b/.editorconfig
index dfe2a8a..85e09e7 100644
--- a/.editorconfig
+++ b/.editorconfig
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 root = true
 
 [*]
diff --git a/.envrc b/.envrc
index 9befd39..d1bbbe1 100644
--- a/.envrc
+++ b/.envrc
@@ -1,2 +1,2 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 use flake
diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml
index d39044e..9635f3f 100644
--- a/.github/workflows/agda.yml
+++ b/.github/workflows/agda.yml
@@ -1,5 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
-# (MPL-2.0 is automatic legal fallback until PMPL is formally recognised)
+# SPDX-License-Identifier: MPL-2.0
 
 name: Agda
 
diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml
index 8221b49..faa979b 100644
--- a/.github/workflows/governance.yml
+++ b/.github/workflows/governance.yml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # governance.yml — single wrapper calling the shared estate governance bundle
 # in hyperpolymath/standards instead of carrying per-repo copies.
 #
diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml
index a895ce4..dfacf3b 100644
--- a/.github/workflows/hypatia-scan.yml
+++ b/.github/workflows/hypatia-scan.yml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # Hypatia Neurosymbolic CI/CD Security Scan
 name: Hypatia Security Scan
 
diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml
index e55c1c5..11453f4 100644
--- a/.github/workflows/mirror.yml
+++ b/.github/workflows/mirror.yml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
 name: Mirror to Git Forges
 
diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml
index 8185aa5..073c66c 100644
--- a/.github/workflows/scorecard.yml
+++ b/.github/workflows/scorecard.yml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 name: OSSF Scorecard
 on:
   push:
diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.machine_readable/6a2/AGENTIC.a2ml
index 338851e..dae5ba0 100644
--- a/.machine_readable/6a2/AGENTIC.a2ml
+++ b/.machine_readable/6a2/AGENTIC.a2ml
@@ -14,7 +14,7 @@
 ;;; closed questions, redo superseded work, or violate forbidden
 ;;; rebrandings.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types agentic)
diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/6a2/ECOSYSTEM.a2ml
index b6574a7..83bf926 100644
--- a/.machine_readable/6a2/ECOSYSTEM.a2ml
+++ b/.machine_readable/6a2/ECOSYSTEM.a2ml
@@ -13,7 +13,7 @@
 ;;; session understands echo-types' position in the constellation
 ;;; without re-deriving it.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types ecosystem)
@@ -101,10 +101,11 @@
      (source . "Standing decision sd-003 in STATE.scm")
      (artefacts . (".github/workflows/mirror.yml" "MIRROR_SETUP.adoc")))
 
-    ((convention . "License: PMPL-1.0-or-later for code and docs")
-     (source . "META.scm SPDX header pattern; constellation default")
-     (artefacts . ("LICENSE-PMPL-1.0.txt" ; if present
-                   "SPDX headers in all .scm files")))
+    ((convention . "License: MPL-2.0 for code (PMPL retained as narrative/cultural overlay only; see docs/PMPL-NARRATIVE.adoc — owner direction 2026-05-20)")
+     (source . "META.scm SPDX header pattern; owner direction 2026-05-20 supersedes PMPL-1.0-or-later policy")
+     (artefacts . ("LICENSE" ; MPL-2.0
+                   "docs/PMPL-NARRATIVE.adoc" ; cultural overlay
+                   "SPDX headers in all .a2ml files")))
 
     ((convention . "Cross-platform builds: Linux primary, Windows secondary")
      (source . "Standing decision sd-004 in STATE.scm")
diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml
index 9f9e59d..33a5ac1 100644
--- a/.machine_readable/6a2/META.a2ml
+++ b/.machine_readable/6a2/META.a2ml
@@ -6,7 +6,7 @@
 ;;; Schema reference:
 ;;;   github.com/hyperpolymath/standards/blob/main/meta-a2ml/spec/abnf/meta.abnf
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types meta)
diff --git a/.machine_readable/6a2/NEUROSYM.a2ml b/.machine_readable/6a2/NEUROSYM.a2ml
index 57b52f1..8f46ea4 100644
--- a/.machine_readable/6a2/NEUROSYM.a2ml
+++ b/.machine_readable/6a2/NEUROSYM.a2ml
@@ -13,7 +13,7 @@
 ;;; it implies, and what was deliberately NOT proved (PATH B
 ;;; obligations).
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types neurosym)
diff --git a/.machine_readable/6a2/PLAYBOOK.a2ml b/.machine_readable/6a2/PLAYBOOK.a2ml
index 04f393d..409c30d 100644
--- a/.machine_readable/6a2/PLAYBOOK.a2ml
+++ b/.machine_readable/6a2/PLAYBOOK.a2ml
@@ -14,7 +14,7 @@
 ;;; (architectural decisions) and gated by AGENTIC.scm. PLAYBOOKs
 ;;; introduce no new authority; they execute permitted plans.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types playbook)
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
index 599547c..5fa17fc 100644
--- a/.machine_readable/6a2/STATE.a2ml
+++ b/.machine_readable/6a2/STATE.a2ml
@@ -12,7 +12,7 @@
 ;;; concluded; the verdict is negative; the documentation cascade has been
 ;;; applied; the recipe is no longer a candidate locus of distinctness.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types ei-2 state)
@@ -36,7 +36,7 @@
     (canonical-host . github)                ; per current forge workflow
     (mirrors        . (gitlab codeberg))
     (version-target . "0.1.1")
-    (license        . "PMPL-1.0-or-later")))
+    (license        . "MPL-2.0")))
 
 ;;; ============================================================
 ;;; Session header
diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
index 1b470cd..a94699a 100644
--- a/0-AI-MANIFEST.a2ml
+++ b/0-AI-MANIFEST.a2ml
@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; 0-AI-MANIFEST.a2ml — echo-types
 
 [ai-contract]
diff --git a/Containerfile b/Containerfile
index ac5bc0c..3987ba2 100644
--- a/Containerfile
+++ b/Containerfile
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # Containerfile — podman-build fallback when stapeln is unavailable.
 
 # TODO(scaffold): pin @sha256
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
index 19fd7d2..c80451f 100644
--- a/EXPLAINME.adoc
+++ b/EXPLAINME.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = echo-types: explain me
 :icons: font
 
diff --git a/QUICKSTART-DEV.adoc b/QUICKSTART-DEV.adoc
index 004caf0..8b49fdc 100644
--- a/QUICKSTART-DEV.adoc
+++ b/QUICKSTART-DEV.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = QUICKSTART-DEV: echo-types
 :toc:
 
diff --git a/QUICKSTART-MAINTAINER.adoc b/QUICKSTART-MAINTAINER.adoc
index 8f6c443..4c1eaa3 100644
--- a/QUICKSTART-MAINTAINER.adoc
+++ b/QUICKSTART-MAINTAINER.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = QUICKSTART-MAINTAINER: echo-types
 :toc:
 
diff --git a/QUICKSTART-USER.adoc b/QUICKSTART-USER.adoc
index 88aa474..dc50d55 100644
--- a/QUICKSTART-USER.adoc
+++ b/QUICKSTART-USER.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = QUICKSTART-USER: echo-types
 :toc:
 
diff --git a/README.md b/README.md
index 941bac5..5328a79 100644
--- a/README.md
+++ b/README.md
@@ -1,10 +1,10 @@
-<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- SPDX-License-Identifier: MPL-2.0 -->
 <!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 
 # echo-types
 
 [![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/echo-types)
-[![License: PMPL-1.0](https://img.shields.io/badge/License-PMPL--1.0-blue.svg)](https://github.com/hyperpolymath/palimpsest-license)
+[![License: MPL-2.0](https://img.shields.io/badge/License-MPL--2.0-blue.svg)](https://www.mozilla.org/en-US/MPL/2.0/)
 [![Green Web](https://api.thegreenwebfoundation.org/greencheckimage/github.com)](https://www.thegreenwebfoundation.org/green-web-check/?url=github.com)
 
 Constructive Agda development for echo types as a first-class notion of structured loss:
diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc
index 6ee64c4..70f96bc 100644
--- a/TOPOLOGY.adoc
+++ b/TOPOLOGY.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = echo-types: topology
 :toc:
 
diff --git a/arghda-core/Cargo.toml b/arghda-core/Cargo.toml
index 873b67b..db86e92 100644
--- a/arghda-core/Cargo.toml
+++ b/arghda-core/Cargo.toml
@@ -3,7 +3,7 @@ name = "arghda-core"
 version = "0.1.0"
 edition = "2021"
 description = "Lightweight proof-workspace manager for Agda"
-license = "PMPL-1.0-or-later"
+license = "MPL-2.0"
 repository = "https://github.com/hyperpolymath/echo-types"
 
 [[bin]]
diff --git a/contractiles/Dustfile.a2ml b/contractiles/Dustfile.a2ml
index d4c8527..2efb481 100644
--- a/contractiles/Dustfile.a2ml
+++ b/contractiles/Dustfile.a2ml
@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Dustfile.a2ml — recovery & rollback for echo-types.
 
 (contractile :kind dust :version 1)
diff --git a/contractiles/Intentfile.a2ml b/contractiles/Intentfile.a2ml
index e4be92b..f482a84 100644
--- a/contractiles/Intentfile.a2ml
+++ b/contractiles/Intentfile.a2ml
@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Intentfile.a2ml — declared future intent for echo-types.
 
 (contractile :kind intent :version 1)
diff --git a/contractiles/Mustfile.a2ml b/contractiles/Mustfile.a2ml
index 3d3f6c6..22e3f22 100644
--- a/contractiles/Mustfile.a2ml
+++ b/contractiles/Mustfile.a2ml
@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Mustfile.a2ml — physical state invariants for echo-types.
 
 (contractile :kind must :version 1)
diff --git a/contractiles/Trustfile.a2ml b/contractiles/Trustfile.a2ml
index 0581662..efa3714 100644
--- a/contractiles/Trustfile.a2ml
+++ b/contractiles/Trustfile.a2ml
@@ -1,11 +1,11 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Trustfile.a2ml — integrity & provenance for echo-types.
 
 (contractile :kind trust :version 1)
 
 (trust license-content
   :doc "LICENSE contains expected SPDX identifier."
-  :cmd "grep -q 'PMPL\\|License' LICENSE")
+  :cmd "grep -q 'Mozilla Public License' LICENSE")
 
 (trust no-secrets-committed
   :doc "No credential files committed."
diff --git a/docs/PMPL-NARRATIVE.adoc b/docs/PMPL-NARRATIVE.adoc
new file mode 100644
index 0000000..a864230
--- /dev/null
+++ b/docs/PMPL-NARRATIVE.adoc
@@ -0,0 +1,106 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+= PMPL as Narrative Overlay
+:toc: macro
+:toclevels: 2
+:sectnums:
+:icons: font
+
+[.lead]
+This repository is licensed under *MPL-2.0* (see `LICENSE`). The
+*PMPL* (Palimpsest-MPL) name remains as a *narrative / cultural /
+discipline overlay* documented here, NOT as an SPDX identifier and
+NOT as a separate legal text. This file exists to record what the
+PMPL framing contributes that the bare MPL-2.0 identifier does not.
+
+== Policy in one paragraph
+
+*Stated licence (legal):* MPL-2.0. This is the licence the SPDX
+headers carry, the LICENSE file contains, the README badge displays,
+and downstream consumers / registries / scanners see. There is no
+"PMPL-1.0-or-later" SPDX identifier in this repository.
+
+*PMPL (narrative):* the working-discipline framing under which this
+code was developed. Palimpsest-MPL was, in its prior incarnation, an
+overlay licence whose text incorporated MPL-2.0 by reference. The
+owner direction of 2026-05-20 collapsed the overlay into MPL-2.0
+proper and lifted the *posture* it represented into this narrative
+document. No legal content was lost: PMPL's operative legal effect
+*was* MPL-2.0 (lawyer-confirmed). What was discarded is a stated
+SPDX identifier that registries, scanners, and downstream tooling
+treated as foreign.
+
+== What PMPL represented
+
+The Palimpsest framing carried three commitments that survive intact
+under MPL-2.0:
+
+. *Multi-author authorship as the default reading.* "Palimpsest"
+  named the working assumption that a meaningful body of code is
+  *layered*: contributions overwrite, gloss, and re-purpose
+  predecessors, and the licence regime should reflect that no single
+  author owns the latest layer cleanly. MPL-2.0's file-level
+  copyleft realises exactly this: each file is its own unit, and the
+  layering is visible in the file's history.
+. *Source availability as a discipline, not a strategy.* PMPL was
+  written to make source release the *default* rather than an
+  opt-in. MPL-2.0's "any covered file you distribute, you make the
+  source available for" clause is the operative version of the same
+  commitment.
+. *Narrative coherence over registry convenience.* PMPL's text spent
+  prose on the *why* of its terms; MPL-2.0 spends none. This
+  document is where the *why* now lives, divorced from the legal
+  text it used to be attached to.
+
+== What we no longer claim
+
+. *That PMPL is a distinct licence at registries.* It never was at
+  any standard SPDX registry. crates.io, npm, Hackage, Debian's
+  copyright scanners and similar all treated `PMPL-1.0-or-later` as
+  foreign and required an OSI-recognised fallback (which is
+  precisely MPL-2.0). Carrying both identifiers was friction
+  without legal effect.
+. *That there is a separate Palimpsest copyleft regime.* There
+  isn't. The legal regime is MPL-2.0; the working discipline that
+  PMPL named is documented here.
+. *That `palimpsest-license` is a co-licensing dependency.* It is
+  reference-only documentation of the prior framing. Downstream
+  consumers do not need to read it.
+
+== Header convention going forward
+
+Source files carry exactly:
+
+[source]
+----
+SPDX-License-Identifier: MPL-2.0
+SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+----
+
+No `PMPL-1.0-or-later`, no compound `MPL-2.0 OR …` clauses, no
+inline comment explaining "MPL-2.0 is the legal fallback for PMPL".
+The header is the legal statement; this document is the narrative.
+Authoring new files: use the two lines above verbatim (substitute
+copyright holder as appropriate); do not invent overlays.
+
+== History
+
+* *Prior to 2026-05-20*: `PMPL-1.0-or-later` was the stated SPDX
+  identifier across this and ~69 other repositories in the estate.
+  MPL-2.0 was named as the automatic legal fallback (lawyer-confirmed).
+* *2026-05-20 (owner direction)*: collapse the SPDX identifier to
+  MPL-2.0; preserve the PMPL framing as this narrative document.
+* *Drift note*: SPDX headers across the wider estate may still carry
+  `PMPL-1.0-or-later` and will be migrated in their own time. The
+  legal effect is unchanged (MPL-2.0 is the operative licence in
+  either case); the stated identifier is the only thing that
+  differs. Migration is owner-paced and manual.
+
+== References
+
+* `LICENSE` (MPL-2.0 full text, this repository).
+* `LICENSE-docs` (CC-BY-4.0 full text for documentation, this
+  repository).
+* Mozilla Public License v2.0 — https://www.mozilla.org/en-US/MPL/2.0/
+* SPDX licence list — https://spdx.org/licenses/MPL-2.0.html
diff --git a/docs/echidna-design-search-2026-04-28.adoc b/docs/echidna-design-search-2026-04-28.adoc
index 533f207..c1c9253 100644
--- a/docs/echidna-design-search-2026-04-28.adoc
+++ b/docs/echidna-design-search-2026-04-28.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = Echidna design-search findings — Phase 1.3 + unbudgeted wf-<ᵇʳᶠ_
 :date: 2026-04-28
 :toc:
diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc
index 959b0c7..75a8314 100644
--- a/docs/echo-types/MAP.adoc
+++ b/docs/echo-types/MAP.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = echo-types: Master Map
 :toc: macro
diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc
index fafcec6..b8a46e3 100644
--- a/docs/echo-types/echo-kernel-note.adoc
+++ b/docs/echo-types/echo-kernel-note.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = echo-types: kernel vs derived (one-page note)
 :toc: macro
diff --git a/flake.nix b/flake.nix
index a9b3158..7e538ea 100644
--- a/flake.nix
+++ b/flake.nix
@@ -1,5 +1,5 @@
 {
-  # SPDX-License-Identifier: PMPL-1.0-or-later
+  # SPDX-License-Identifier: MPL-2.0
   #
   # Reproducible toolchain for echo-types — foundation P1 (CI-via-flake
   # exact pin; docs/foundation.adoc §"Known limitations").
diff --git a/scripts/kernel-guard.sh b/scripts/kernel-guard.sh
index 2cbea84..69b579a 100644
--- a/scripts/kernel-guard.sh
+++ b/scripts/kernel-guard.sh
@@ -1,6 +1,5 @@
 #!/bin/sh
-# SPDX-License-Identifier: PMPL-1.0-or-later
-# (MPL-2.0 is automatic legal fallback until PMPL is formally recognised)
+# SPDX-License-Identifier: MPL-2.0
 #
 # kernel-guard.sh — enforce the EchoKernel funext-free certificate and
 # keep docs/echo-types/echo-kernel-note.adoc honest.
diff --git a/stapeln.toml b/stapeln.toml
index 4de13f9..29abf57 100644
--- a/stapeln.toml
+++ b/stapeln.toml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # stapeln.toml — layered Chainguard container build for echo-types.
 # Echo-types is a proof library, not a service. The container is an artefact carrier:
 # it bundles type-checked Agda artefacts (.agdai) for downstream consumers to mount.
@@ -8,7 +8,7 @@ name = "echo-types"
 version = "0.1.0-alpha"
 description = "Constructive Agda formalisation of echo types"
 author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
-license = "PMPL-1.0-or-later"
+license = "MPL-2.0"
 registry = "ghcr.io/hyperpolymath"
 
 [build]
diff --git a/tools/check-guardrails.sh b/tools/check-guardrails.sh
index 22ece83..ec64bda 100644
--- a/tools/check-guardrails.sh
+++ b/tools/check-guardrails.sh
@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 #
 # Foundation guardrail (added 2026-05-18 — the long-documented
 # "CI-grep-enforced" check that did not previously exist).