docs: restore composition-iso evidence under post-EI-2 framing

The 5d1e679 / e608ace adjacency refresh on main introduced
per-neighbour composition-iso evidence (Echo-comp-iso,
cancel-iso, projection-pentagon) and a cross-cutting
"Compositional evidence (load-bearing across notes)" section
in the README. The e8b11fb adjacency restructure ("two
argument families: truncation + 2-cell") was authored against
the pre-5d1e679 base and silently dropped that content from
the three rewritten files (README, hott-fibers,
refinement-types) — while the four files e8b11fb did not
touch (cubical-systems, lenses-and-optics,
provenance-semirings, setoid-quotients) retained their
5d1e679 citations.

Under EI-2's negative termination, the iso family's role
splits two ways:

ROLE A (subsumed). The 5d1e679 README section was framed as
evidence "load-bearing across notes" — a cross-cutting
summary that EI-2 has narrowed away from. The section header
stays dropped; the per-neighbour content it pointed at lives
in the per-neighbour notes themselves, which is the
post-EI-2-correct location.

ROLE B (preserved). The iso family is also per-neighbour
structural evidence: composition without higher equalities
(hott-fibers) and Σ-shape isolating intermediate points as
proof-relevant data (refinement-types) both strengthen the
truncation argument specifically. Reinstated as new
"Composition-iso evidence" sections in hott-fibers.adoc and
refinement-types.adoc, framed as supporting the truncation
argument rather than as cross-axis integration evidence.

EI2_REPORT.adoc gains a paragraph in the Status section
documenting the role split (applied in the EI-2 termination
commit that this commit precedes).

No formal results change; only the role they play in the
gate-1 argument.

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

Author: hyperpolymath

docs/adjacency/hott-fibers.adoc

@@ -65,6 +65,40 @@ fiber) vs. propositionally-truncated fiber". HoTT *contains*
 both; the win is over a specific applied use of HoTT, not over
 HoTT itself.
 
+== Composition-iso evidence
+
+Beyond the `echo-not-prop` witness-loss certificate, the iso
+family in `proofs/agda/Echo.agda` provides structural evidence
+for the proof-relevant-vs-truncated distinction under
+composition:
+
+* `Echo-comp-iso-{to, from, from-to, to-from}` exhibits
+  `Echo (g ∘ f) y ≃ Σ b. Echo f b × (g b ≡ y)` with both
+  round-trips on the nose.
+* `cancel-iso-{to, from}` reduce composition through a section
+  to composition through the underlying fiber, when the outer
+  step admits a pointwise inverse.
+* `Echo-comp-iso-pent-{B, echo}` show 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 plain
+Agda with a deliberately minimal `--without-K` proof. Under
+propositional truncation the family collapses (Σ becomes ∃, and
+the round-trip equations become automatic since the targets are
+propositions); in the un-truncated form, the family preserves
+witness identity under composition. Together with
+`echo-not-prop`, this is the second structural distinction
+between proof-relevant fibres and truncated fibres: not just
+that the witness data is present, but that it composes without
+intermediate higher-equalities.
+
+The fact is structural about Echo-as-fiber and is independent
+of EI-2's negative termination — it distinguishes proof-relevant
+fibres from truncated fibres regardless of what the integration
+recipe does or doesn't do.
+
 == 2-cell argument
 
 In HoTT (or cubical Agda), 2-cells between parallel fibers are

docs/adjacency/refinement-types.adoc

@@ -63,6 +63,45 @@ This is the right shape of claim for this neighbour: explicitly
 acknowledge the tied case; carry the win against the
 propositional case as the formal exhibit.
 
+== Composition-iso evidence
+
+Beyond the `echo-not-prop` witness-loss certificate, the iso
+family in `proofs/agda/Echo.agda` provides a structural analogue
+that strengthens the truncation argument specifically against
+propositional-predicate refinement:
+
+* `Echo-comp-iso-{to, from, from-to, to-from}` proves
+  `Echo (g ∘ f) y ≃ Σ b. Echo f b × (g b ≡ y)` directly.
+* With a bijection on the outer leg, `cancel-iso-{to, from}`
+  exhibit 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.
+
+Under Σ-relevant refinement (Agda, Coq), the predicate IS the
+refinement type and the iso family is the same family, not a
+separate result — the tied case acknowledged in "Distinctness
+claim" above. Under propositional-predicate refinement, the
+predicate cannot isolate the intermediate `b` as data without
+becoming type-relevant, at which point it has left propositional
+refinement. So the iso family is structural evidence that the
+truncation argument is tracking the right axis: what
+propositionally-truncated refinement loses under composition is
+not a corner case but a load-bearing structural property of
+Echo-as-Σ-family.
+
+The fact is structural about Echo-as-Σ and is independent of
+EI-2's negative termination — it strengthens the truncation
+argument's distinctness against propositional-predicate
+refinement regardless of what the integration recipe does or
+doesn't do.
+
 == 2-cell argument
 
 Not directly applicable. Refinement-type systems do not, in