docs(gate-1): refresh adjacency notes with composition-iso evidence

Refresh Gate 1 adjacency notes to cite the composition-track theorems
that landed since the original drafts: Echo-comp-iso-{to, from,
from-to, to-from}, cancel-iso-{to, from}, and projection-pentagon
Echo-comp-iso-pent-{B, echo} in proofs/agda/Echo.agda. These are
content distinguishing echo types from refinement, lens/optic, HoTT-
fiber, setoid-quotient, provenance-semiring, and cubical neighbours.

Normalise cubical-systems.adoc to the canonical 5-section template
the other notes use (1. Nearest construction, 2. What do echo types
add, 3. What do they not add, 4. Honest risk, 5. Verdict for Gate 1)
so all six notes discharge the Gate 1 test in the same shape.

Add a "Compositional evidence (load-bearing across notes)" section to
the README pointing at the iso family and cancellation, since these
are now cited from multiple notes.

Verdicts unchanged: refinement-types, lenses-and-optics, setoid-
quotients, provenance-semirings, cubical-systems all survive Gate 1;
hott-fibers remains a marginal pass dependent on Gate 2/3 outcomes.
The refresh strengthens the supporting evidence rather than reopening
the verdicts.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/adjacency/README.adoc

@@ -61,3 +61,20 @@ All notes are written against the current Agda development
 (`--safe --without-K`, no postulates). Claims reference specific
 theorems by module and name. Anything not backed by a compiled
 theorem is called out as conjectural.
+
+== Compositional evidence (load-bearing across notes)
+
+Two families of theorems in `proofs/agda/Echo.agda` are cited across
+multiple notes as content distinguishing echo types from neighbours:
+
+* *Base-accumulation iso.* `Echo-comp-iso-{to, from, from-to, to-from}`
+  proves `Echo (g ∘ f) y ≃ Σ b. Echo f b × (g b ≡ y)` with both
+  round-trips, plus the projection-pentagon lemmas
+  `Echo-comp-iso-pent-{B, echo}` for three-fold composites.
+* *Cancellation under section/retraction.* `cancel-iso-{to, from}`
+  exhibit `Echo (g ∘ f) y → Echo f (s y)` and back when `g` admits a
+  pointwise inverse `s`, without needing a triangle-identity coherence
+  for the partial maps.
+
+Each adjacency note flags whichever of these is load-bearing for its
+particular framework comparison.

docs/adjacency/cubical-systems.adoc

@@ -3,57 +3,97 @@
 
 toc::[]
 
-== 1. Nearest existing constructions
+== 1. Nearest existing construction
 
 The nearest cubical-side systems for this repository are:
 
 * Cubical Agda: Agda's built-in `--cubical` mode plus the separate
-  Cubical Agda library.
+  Cubical Agda library, supplying first-class path types, higher
+  inductive types, and a definitional univalence principle.
 * `RedPRL`: a tactic-oriented assistant for computational Cartesian
   cubical type theory.
 * `redtt` and `cooltt`: experimental cubical proof assistants /
-  typecheckers.
+  typecheckers in the same family.
 
 For this repository, Cubical Agda is the closest operational neighbour:
-it preserves the Agda language and keeps the migration cost lower than a
-move to a different prover.
+it preserves the Agda language and would keep the migration cost lower
+than a move to a different prover. The relevant cubical construction
+itself is the same sigma-of-equation, `Σ x , (f x = y)`, but read
+against path equality rather than `Relation.Binary.PropositionalEquality`.
 
-== 2. What do they add?
+== 2. What do echo types add?
 
-* First-class path/cubical equality and higher-dimensional structure.
-* Higher inductive and quotient-like reasoning that plain
-  `--safe --without-K` Agda does not provide directly.
-* A plausible route for roadmap item `R2` in `roadmap.adoc`: treating
-  indistinguishability with equivalence-aware identity rather than only
-  propositional/set-level relations.
+. *Plain intensional setting, deliberately.* The Agda development uses
+  `--safe --without-K` and keeps `_≡_` as ordinary
+  propositional equality. `EchoCharacteristic.echo-true≢echo-false`
+  exploits exactly that: it is a disequality of two inhabitants of the
+  same fiber that a cubical reader, working up to higher equivalence,
+  would not recover automatically. The retained witness is meaningful
+  because the equality is _not_ identifying it.
+. *Composition machinery proved by `refl`/`cong`/`trans`.* The
+  recently-landed `Echo-comp-iso-{to, from, from-to, to-from}` in
+  `proofs/agda/Echo.agda` gives a base-accumulation isomorphism
+  `Echo (g ∘ f) y ≃ Σ b. Echo f b × (g b ≡ y)` directly in plain
+  Agda. `cancel-iso-{to, from}` and the projection-pentagon lemmas
+  `Echo-comp-iso-pent-{B, echo}` follow the same pattern. A cubical
+  setting would supply more powerful tools (path induction, transport
+  along univalence) but is not _required_ for these statements; they
+  hold without higher-dimensional machinery.
+. *Residue / graded / linear / epistemic stack.* `EchoResidue`,
+  `EchoGraded`, `EchoLinear`, `EchoEpistemic`, `EchoIntegration` build
+  the structured-loss hierarchy without HITs, truncations, or path
+  algebra. A cubical reformulation would not, by itself, supply this
+  stack; it would be a re-host of content that already lives in plain
+  Agda.
 
-== 3. What do they _not_ add?
+== 3. What do echo types _not_ add?
 
-* No automatic reuse guarantee for the current Buchholz work. Moving to
-  `RedPRL`, `redtt`, or `cooltt` is a prover migration, not a local
-  refactor.
-* No evidence yet that the blocked direct same-binder route in plain
-  Agda disappears automatically in a cubical setting.
-* No requirement for the current echo-types evidence base, which still
-  compiles in plain Agda with the standard library.
+* No path/cubical equality, no higher-dimensional structure, no HITs.
+* No quotient _types_, no automatic respect-of-relations through
+  univalence.
+* No direct route for roadmap item `R2` of `roadmap.adoc`
+  (equivalence-aware indistinguishability), which is plausibly best
+  expressed cubically. That work is tracked as a future migration, not
+  as a current claim.
+* No reuse guarantee for the Buchholz / ordinal track if the prover
+  changes. Moving to `RedPRL`, `redtt`, or `cooltt` would be a prover
+  migration rather than a local refactor.
 
-== 4. Working decision
+== 4. Honest risk to the distinction
 
-* Active repository tooling stays Agda-first.
-* Optional exploratory extension: Agda `--cubical` plus the Cubical
-  Agda library.
-* `RedPRL`, `redtt`, and `cooltt` are tracked as adjacent references,
-  not installed or required for normal builds.
+The sharpest cubical-side reading is: "every echo theorem is a
+shadow of a cubical statement; what you call an `_≡_` proof is a
+0-dimensional path, and your insistence on intensional equality is a
+self-imposed restriction without mathematical content." Under that
+reading, echo types are just fibers in plain Agda, awaiting a port to
+a cubical assistant where the proofs would be cleaner.
 
-== 5. Why this matters here
+The reply is that the deliberately-intensional setting is _what
+generates the structured-loss content_:
+`echo-true≢echo-false`, `state₁≢state₂`, and
+`no-section-collapse-to-residue` rely on intensional equality being
+non-trivial. A cubical port would have to add explicit truncation
+levels to recover the same proof-relevance distinctions, at which
+point the echo development reappears as a 0-truncated specialisation
+of the cubical theory. The framing question — "study fibers in plain
+Agda with structured loss" vs. "study fibers cubically with chosen
+truncation" — is editorial; both are coherent.
 
-Cubical systems may matter later for quotient-like or
-equivalence-sensitive extensions of echo types, especially roadmap item
-`R2`. They are not part of the evidential base for the current identity
-claim. That claim still stands or falls on the plain-Agda development
-already in the repository.
+The current development asserts that the plain-Agda framing is the
+right base camp, with cubical extensions as an optional later step.
 
-== 6. References
+== 5. Verdict for Gate 1
+
+Survives. Cubical systems are an _extensional richer_ neighbour rather
+than a refutation: they could host an echo development with stronger
+equality, but they do not subsume the structured-loss machinery, and
+the bare type former `Σ x , f x = y` is identical content under either
+reading. The identity claim does not stand on cubical avoidance; it
+stands on the residue / graded / linear / epistemic stack and on the
+composition / cancellation / pentagon rungs proved without higher-path
+machinery.
+
+== References
 
 * Cubical Agda library: `https://github.com/agda/cubical`
 * `RedPRL` family: `https://redprl.org/`

docs/adjacency/hott-fibers.adoc

@@ -35,6 +35,20 @@ on top of it.
   `map-over-comp` is a rewrite on `trans-assoc`; the square proof
   `map-square` uses only `cong` and `trans`. These are reusable
   outside of a HoTT library.
+. *Base-accumulation isomorphism, cancellation, and projection
+  pentagon, proved intensionally.* `Echo-comp-iso-{to, from, from-to,
+  to-from}` proves
+  `Echo (g ∘ f) y ≃ Σ b. Echo f b × (g b ≡ y)` with both round-trips
+  on the nose; `cancel-iso-{to, from}` give the section / retraction
+  reduction in both directions when `g` admits a pointwise inverse;
+  `Echo-comp-iso-pent-{B, echo}` show the two natural three-fold
+  factorings agree by `refl` on the A-origin and the inner echo.
+  These are not new HoTT results — they are corollaries of
+  Σ-associativity and J — but they ship as named theorems in the echo
+  development, with a deliberately minimal `--without-K` proof, and
+  feed the residue / graded / linear bridges below. A standard HoTT
+  library would re-derive them through transport; the echo version is
+  reusable wherever ordinary intensional equality is enough.
 . *Residue, graded, linear, epistemic extensions sit on top of the
   intensional core.* Modules `EchoResidue`, `EchoGraded`,
   `EchoLinear`, `EchoEpistemic`, `EchoIntegration` do not require

docs/adjacency/lenses-and-optics.adoc

@@ -42,6 +42,16 @@ the "first projection lens" `_1 : Lens (A × B) A`.
   square `f' ∘ u ≡ v ∘ f`. This is adjacent to lens composition but
   the morphism data is different: morphisms of source and target
   codomains plus a coherence, not a get/put pair at each step.
+  Sequential composition has its own theorem:
+  `Echo-comp-iso-{to, from, from-to, to-from}` exhibits
+  `Echo (g ∘ f) y ≃ Σ b. Echo f b × (g b ≡ y)`, with the projection-
+  pentagon lemmas `Echo-comp-iso-pent-{B, echo}` enforcing coherence
+  for three-fold composites. Lenses ship the analogous "compose two
+  lenses to get a lens" as a definition; echoes ship it as an
+  isomorphism theorem in plain Agda. `cancel-iso-{to, from}`
+  additionally captures the optic intuition "if the outer step is
+  invertible, peel it off" as `Echo (g ∘ f) y → Echo f (s y)` and
+  back, _without_ requiring a `put` half.
 . *Residue as first-class lowering.* `EchoResidue.echo-to-residue`
   lowers a full echo to a certificate, with
   `no-section-collapse-to-residue` witnessing strict loss. Lenses

docs/adjacency/provenance-semirings.adoc

@@ -33,9 +33,10 @@ collapsing computation" is in the same genre.
   types indexed by observer.
 . *Graded degradation with composition.* `EchoGraded.degrade-comp`
   in `proofs/agda/EchoGraded.agda` composes lowerings along
-  `_≤g_`. K-provenance has a natural homomorphism story ("evaluate in
-  a simpler semiring"), but a homomorphism between semirings is a
-  different mathematical object from a typed lowering of witnesses.
+  `_≤g_`. K-provenance has a natural homomorphism story ("evaluate
+  in a simpler semiring"), but a homomorphism between semirings is
+  a different mathematical object from a typed lowering of witnesses
+  indexed over a pre-order on grades.
 . *Strict non-recoverability as a theorem.*
   `no-section-collapse-to-residue` in `EchoResidue` _proves_ that the
   lowering from echo to residue has no inverse. Provenance

docs/adjacency/refinement-types.adoc

@@ -48,6 +48,17 @@ current development:
   with no section. Refinement-type presentations usually collapse at
   the propositional level and do not admit an analogous hierarchy of
   strictly weaker certificates.
+. *Compositional structure as theorems, not as user-supplied glue.*
+  `Echo-comp-iso-{to, from, from-to, to-from}` in `proofs/agda/Echo.agda`
+  proves `Echo (g ∘ f) y ≃ Σ b. Echo f b × (g b ≡ y)` directly. With a
+  bijection on the outer leg, `cancel-iso-{to, from}` exhibits the
+  cancellation `Echo (g ∘ f) y → Echo f (s y)` and back; the projection-
+  pentagon lemmas `Echo-comp-iso-pent-{B, echo}` show two natural
+  three-fold factorings agree. None of this is standard refinement-type
+  machinery: refinement subsets have no ambient theorem stating that
+  `{ x | (g ∘ f) x = y }` is canonically isomorphic to a Σ over an
+  intermediate refinement, because the predicate carrier does not
+  isolate the intermediate point as proof-relevant data.
 
 == 3. What do echo types _not_ add?
 
@@ -71,10 +82,15 @@ echo types as such.
 The residue-based strict weakening in `EchoResidue` is the part most
 resistant to this reading: a refinement type has no natural
 counterpart to "lower to a certificate, and prove no section exists".
-That is where the identity claim, if it survives, is load-bearing.
+The composition-iso family is the second load-bearing piece: it
+states a property of the family `Echo f` that has no obvious
+refinement-subset counterpart unless one re-imports dependent-pair
+machinery, at which point the refinement reading is no longer
+faithful.
 
 == 5. Verdict for Gate 1
 
 Survives, with caveat: the distinction from refinement types rests
-materially on (a) the family indexing by `f` and (b) the residue
-hierarchy, rather than on the subset-type form itself.
+materially on (a) the family indexing by `f`, (b) the residue
+hierarchy, and (c) the composition / cancellation / pentagon iso
+family — rather than on the subset-type form itself.

docs/adjacency/setoid-quotients.adoc

@@ -38,7 +38,15 @@ be read as "quotient by the kernel of `f`".
   `degrade-comp` compose lowerings in a pre-ordered family. A
   setoid presentation would need one relation per grade and explicit
   respect proofs; the graded presentation collapses this into a
-  single function family indexed by `g₁ ≤g g₂`.
+  single function family indexed by `g₁ ≤g g₂` with composition
+  pinned by `refl`.
+. *Functorial composition for the family itself.* `Echo-comp-iso-*`
+  in `proofs/agda/Echo.agda` exhibits `Echo (g ∘ f) y` as
+  isomorphic to `Σ b. Echo f b × (g b ≡ y)`, with pentagon coherence
+  for three-fold composites. This is structure on the _family_
+  `Echo f`, not on a setoid carrier; a setoid translation would need
+  to carry the equivalence relation through the iso explicitly,
+  losing the reading "echoes glue along the intermediate visible".
 
 == 3. What do echo types _not_ add?