docs: rule out 2-categorical shape; credit landed EchoApprox + EchoDecidable in roadmap

hyperpolymath · claude · hyperpolymath · commit 0a8ae26b1e83 · 2026-05-20T14:45:22.000+01:00
Doc-only sweep on the echo-types theory tree. Four pieces:

1. New closure note `docs/echo-types/decisions/no-2-cat.adoc` —
   verdict / evidence / implication for the roadmap entry
   "2-categorical shape: commit or rule out". Every would-be
   2-cell in the landed code is `refl` or forced trivial by
   propositionality (`≤g-prop`, `⊑-prop`, `Echo-comp-iso` round-
   trips, pentagon projections, `SliceHom`↔cone, `bridge-natural`).
   The question is closed; future composition write-ups need not
   hedge for a 2-cat refinement.

2. `docs/echo-types/roadmap.md` — Axis 2 entry promoted from
   `[unblocked]` to `[landed]` crediting `EchoApprox.agda`
   (ε-fibre over `Tolerance` + `PseudoMetric` with three headline
   lemmas); Axis 8 entry lists three remaining candidates (not
   four — decidability-respecting has shipped as
   `EchoDecidable.agda`); 2-categorical-shape entry replaced with
   `[ruled out — see decisions/no-2-cat.adoc]`.

3. `docs/echo-types/composition.md` — §Q1 closed as rule-out
   pointing to the decisions note; §Q4 "evidence" language
   strengthened to "definitive characterisation"; §Q6 hedge
   "expressible as a 2-cell in the hypothetical 2-category"
   reformulated as a 1-categorical slice-morphism / fibration-
   section question.

4. `docs/echo-types/establishment-plan.adoc` + paper.adoc —
   minimal cross-references only (one-line note under the H2
   verdict, NOTE placeholder under the Related work [EXPAND]).
   No spine rewrites. paper.adoc 2-cat-related [EXPAND] tags
   addressed; non-2-cat [EXPAND] tags untouched (own campaign).

Verification: `git diff --stat` shows only doc files; no .agda
touched. asciidoctor not available locally, so render check
deferred — adoc syntax inspected by hand.

Refs roadmap entries; does not Close any GitHub issue.

Co-Authored-By: Claude Opus 4.7 (1M context) &lt;noreply@anthropic.com&gt;
diff --git a/docs/echo-types/composition.md b/docs/echo-types/composition.md
@@ -113,16 +113,20 @@ composition *accumulates* witnesses rather than losing them.
 
 ## Open questions
 
-### Q1. 2-categorical structure
-
-*Question.* Is there a 2-category whose objects are types, whose
-1-morphisms are maps, and whose 2-morphisms are echo-preserving
-transformations? `EchoCategorical.agda` hints at this but does not
-commit to a full 2-categorical axiomatisation.
-
-*Why it matters.* If yes, the composition laws are the coherence
-laws of the 2-category. If no, the composition laws are ad-hoc and
-probably a sign the residue structure is subtler than we modelled.
+### Q1. 2-categorical structure — closed (rule-out)
+
+*Verdict.* No 2-category. The five structurally plausible
+organisations (echo as a lax/oplax 2-functor; slice-of-echos
+with `IsMediator` cells; double category; graded bicomonad;
+Grothendieck stack) each collapse to existing 1-cat +
+graded-comonad + pullback content because every would-be 2-cell
+appears as `refl` or is prop-forced trivial by `≤g-prop` /
+`⊑-prop`. The composition laws (accumulation iso, cancel-iso,
+pentagon Σ-assoc, decoration commuting) are *not* 2-coherence
+laws of a hypothesised 2-category — they are the 1-categorical
+composition laws of a pullback-presented type, full stop. See
+`docs/echo-types/decisions/no-2-cat.adoc` for the full closure
+note (verdict / evidence / implication).
 
 ### Q2. Negative echoes
 
@@ -175,14 +179,18 @@ packaged as a stdlib `Function.Bundles._↔_` via
 once `g b ≡ c` has been pinned, so this is a strict iso inside
 `--safe --without-K`.
 
-*Evidence this is the right shape.* Both lemmas land as `refl`
+*Confirmed this is the right shape.* Both lemmas land as `refl`
 without any `trans-assoc` / `cong-trans` manipulation, because
 `Echo-comp-iso-to`'s body `(x , p) ↦ (f x , (x , refl) , p)` is
 structurally symmetric in the outer function — the f-component
 and witness do not depend on which outer is peeled off. If the
 iso had a `trans`-shaped body instead, pentagon would have
-required real coherence lemmas; the `refl` outcome is evidence
-the iso has the right design.
+required real coherence lemmas. The `refl` outcome is the
+*definitive characterisation*: pentagon is identity — what would
+be the bicategorical associator-2-cell — and is forced trivial
+here. With the 2-cat shape ruled out (§Q1;
+`decisions/no-2-cat.adoc`), this is no longer "evidence the iso
+has the right design" but the 1-categorical-final reading of it.
 
 ### Q5. Interaction with role-indexing, gradings, linearity
 
@@ -204,8 +212,14 @@ preimage `x` and re-applies `f` to reconstruct `y` — the echo is
 temporarily made definite. Does the composition law respect this
 extraction?
 
-*Formalisation hint.* Probably expressible as a 2-cell in the
-hypothetical 2-category of Q1. Not attempted.
+*Formalisation hint (revised).* With the 2-cat shape ruled out
+(§Q1; `decisions/no-2-cat.adoc`), recovery is a 1-categorical
+notion: a slice morphism into `Echo f y` (the extraction step)
+followed by the canonical projection, or equivalently a section
+of the appropriate fibration. The earlier "expressible as a
+2-cell in the hypothetical 2-category of Q1" hedge no longer
+applies. Not attempted; now write-up-tractable on a 1-categorical
+footing.
 
 ---
 
diff --git a/docs/echo-types/decisions/no-2-cat.adoc b/docs/echo-types/decisions/no-2-cat.adoc
@@ -0,0 +1,125 @@
+= D-2026-05-20 — Echo has no 2-categorical shape (rule-out)
+:toc: macro
+:toclevels: 2
+:sectnums:
+:sectnumlevels: 2
+:icons: font
+
+[.lead]
+Closure note for the `roadmap.md` entry
+"2-categorical shape: commit to a 2-category or rule it out"
+and for `composition.md` §Q1 / §Q6. The verdict is *rule out*,
+on argued grounds against the landed Pillars A–D evidence. The
+question is closed; future composition write-ups need not hedge
+for a 2-cat refinement.
+
+toc::[]
+
+== Verdict
+
+Echo's composition / graded-comonad / pullback machinery is
+provably *strict-1-categorical-with-a-thin-graded-fragment*. No
+2-categorical overlay yields a *statable theorem* the existing
+1-cat + graded-comonad + pullback content does not already
+encode at strength equal to or greater than what 2-cells could
+witness. The five structurally plausible 2-cat organisations
+(echo as a lax/oplax 2-functor; slice-of-echos with `IsMediator`
+as 2-cells; double category with `SliceHom` horizontals + cones
+verticals; graded bicomonad; Grothendieck stack of cartesian
+sections) all collapse to existing 1-cat content because every
+would-be 2-cell appears as `refl` or is forced trivial by a
+propositionality hypothesis.
+
+== Evidence (from the landed development)
+
+The "2-cat smells" in the codebase, each resolving trivially:
+
+* *Pentagon Σ-assoc iso* (`Echo.agda` L243–L310). The prototypical
+  bicategorical associator-2-cell. `Echo-comp-iso-pent-B` and
+  `-pent-echo` both close by `refl` on both projections — the
+  would-be associator is identity. Strictly 1-categorical.
+* *`Echo-comp-iso` round-trips* (`Echo.agda` L83–L94). Both
+  `refl`. Strict iso, not pseudo; no unitor data.
+* *`SliceHom` ↔ `EchoCone`* (`EchoPullback.agda` L73–L92). Both
+  round-trips `refl`. A cone *is* a slice morphism by record η —
+  the data is identical; no mediating 2-cell exists.
+* *`echo-pullback-univ`* (`EchoPullback.agda` L55–L134).
+  Uniqueness is *pointwise* (`∀ v → m' v ≡ m v`) — the
+  1-categorical statement minus funext, *not* the 2-cell
+  statement. `IsMediator.coherent` is Σ-second-coherence over
+  the `factor` equation: HoTT pullback-as-Σ shape, not a 2-cell.
+* *`bridge-natural`* (`EchoRelModel.agda` L245–L250). The one
+  real naturality in the suite — `echo-to-graph` between
+  `map-over` and `map-rel` under `relmap-of`. In a 2-cat reading
+  it would be a 2-cell `map-over ⇒ map-rel`; it closes by
+  `refl`. Identity 2-cell; naturality on the nose.
+* *`≤g-prop`* (`EchoGraded.agda` L83–L89). The grade order is
+  propositional: each hom-set is a singleton. In 2-cat language,
+  thin / locally discrete; the graded category enriched in
+  `Prop` *is* a 1-category.
+* *`⊑-prop`* (`EchoRelModel.GradedLossModel`). The interface
+  bakes in propositionality of the loss order. Every instance
+  is thin by signature.
+* *`gcomonad-coassoc`* (`EchoGradedComonad.agda` L126–L150). In
+  a bicomonad, coassoc holds up to an associator 2-cell. Here,
+  on the nose: the common-upper-bound idiom pre-empts the
+  associator (`subst GEcho (⊔g-assoc …)` vanishes because both
+  sides land in the *same* `GEcho g`). The would-be associator
+  is replaced by `≤g-prop`.
+* *`EchoRelModel.GCLaws`*. Model independence proves the comonad
+  laws from `⊑-prop` + composing `reindex` alone; the laws
+  already hold *strictly* in both shipped models. No
+  2-cell-equipped interface is needed.
+
+Every place a 2-cell could appear, it appears as `refl` or is
+forced trivial by a propositionality hypothesis.
+
+== Implication
+
+* `composition.md` §Q1 is closed (rule-out). The composition
+  laws (accumulation iso, cancel-iso, pentagon Σ-assoc,
+  decoration commuting) are promoted from "ad-hoc candidates" to
+  *the complete 1-categorical story* — not 2-coherence laws of a
+  hypothesised 2-category, but the 1-categorical composition
+  laws of a pullback-presented type, full stop.
+* `composition.md` §Q6 (composition in the presence of recovery /
+  echo-erasure) reformulates as a 1-categorical question:
+  recovery as a slice morphism or a fibration section, not a
+  2-cell. Write-up-tractable on this footing.
+* `composition.md` §Q4's "Evidence this is the right shape"
+  upgrades to a *characterisation*: pentagon is `refl` because
+  there is no associator 2-cell to obstruct it.
+* The `EchoGradedComonad` + `EchoRelModel` package is the
+  1-categorical graded-comonad story, not a thin slice toward a
+  bicomonad. The paper draft (`paper.adoc`) need not hedge for
+  a future 2-categorical refinement.
+
+== What would force a reopen (not on the roadmap)
+
+* `MapOver`-up-to-2-cell quantification by a downstream
+  consumer (e.g. ordinal-track collapsing layer needing two
+  `MapOver`s equal up to a 2-cell rather than definitionally).
+  Current decoration families (`EchoApprox`, `EchoChoreo`,
+  `EchoEpistemic`) do not exhibit this.
+* A future grade dropping `≤g-prop` (non-propositional grade
+  lattice carrying genuine semilattice data with non-trivial
+  isos). `EchoSeparating` already shows the characteristic law
+  breaks in that regime — the moment a pseudo / 2-categorical
+  layer becomes content-bearing. Not currently in play.
+* A future third model needing a non-trivial intertwining iso
+  (`model-agreement` currently closes on `refl`).
+* Cubical / HoTT migration (out of `--without-K`) repromoting
+  strict equalities to genuine paths. Out of scope.
+
+None is on the active roadmap. The verdict stands.
+
+== Cross-references
+
+* `docs/echo-types/roadmap.md` — Theory-work entry updated to
+  `[ruled out]`.
+* `docs/echo-types/composition.md` §Q1 / §Q4 / §Q6 — open
+  framings folded into this closure.
+* `docs/echo-types/establishment-plan.adoc` — minimal
+  cross-reference at the H2 verdict / guardrails site.
+* `docs/echo-types/paper.adoc` — related-work `[EXPAND]`
+  carries a placeholder note pointing here.
diff --git a/docs/echo-types/establishment-plan.adoc b/docs/echo-types/establishment-plan.adoc
@@ -288,6 +288,12 @@ rewrite *was* required and has been done (`paper.adoc`,
 `conservativity.adoc`, `types-abstract.adoc`, R-2026-05-18). The
 narrowed thesis (<<thesis>>) is what stands.
 
+NOTE: A 2-categorical refinement of this picture was considered as
+a roadmap-level alternative and *ruled out* on the same evidence
+(every would-be 2-cell appears as `refl` or is prop-forced trivial
+by `≤g-prop` / `⊑-prop`). → ruled out, see
+`decisions/no-2-cat.adoc`.
+
 == Status
 
 [cols="1,4,1", options="header"]
diff --git a/docs/echo-types/paper.adoc b/docs/echo-types/paper.adoc
@@ -339,9 +339,20 @@ 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.
+`echo-pullback-univ` resembles the very-well-behaved *1-lens* laws —
+no 2-cell-equipped optic, see below). Make the novelty crisp: not a
+new object, but a fully mechanised characterisation package with a
+falsifiable-gate methodology.
+
+NOTE: *[2-cat ruled out, see `decisions/no-2-cat.adoc`]* — when the
+related-work pass expands the lens/optic comparison and the
+graded-modality positioning, fold in the 2-categorical rule-out: a
+"bicategorical echo" reading was considered and ruled out on the
+landed evidence (every would-be 2-cell appears as `refl` or is
+prop-forced trivial by `≤g-prop` / `⊑-prop`); the construction
+resembles a very-well-behaved *1-lens*, not a 2-cell-equipped optic.
+The closure note in `decisions/no-2-cat.adoc` is the load-bearing
+artifact; this paragraph should cite it rather than re-argue.
 
 [#reframing-note]
 == Reframing note (2026-05-18)
diff --git a/docs/echo-types/roadmap.md b/docs/echo-types/roadmap.md
@@ -25,19 +25,35 @@ Paths marked **[unblocked]** can proceed today. Paths marked
 
 ## Theory work — no proof assistant needed
 
-- **[unblocked]** Axis 2 (approximate echoes): settle the formal
-  definition before touching Agda. Draft in `taxonomy.md` and
-  `composition.md`.
+- **[landed]** Axis 2 (approximate echoes): formal definition
+  shipped as `proofs/agda/EchoApprox.agda` — an ε-fibre over a
+  parametric `Tolerance` (ordered commutative monoid) and a
+  `PseudoMetric`, with `EchoR ε f y = Σ A (λ x → dist (f x) y ≤
+  ε)` plus the three headline lemmas `echo-approx-intro` (exact
+  ⇒ zero-ε), `echo-approx-relax` (monotone in ε), and
+  `echo-approx-compose` (additive composition under a
+  non-expansive outer leg). Note: the formal definition has been
+  retro-documented from the landed module (follow-up doc PR in
+  lane C tracks the `taxonomy.md` §Axis-2 write-up).
 - **[landed]** Axis 8 (information-theoretic vs computational
-  access): promoted from the candidates list to a numbered axis;
-  four candidate refinements of `Echo` (cost-indexed, graded access
-  modality, decidability-respecting, witness-search abstract
-  machine) are listed. Follow-up: pick one refinement and formalise.
+  access): promoted from the candidates list to a numbered axis.
+  *Three* remaining candidate refinements of `Echo`
+  (cost-indexed, graded access modality, witness-search abstract
+  machine); the *decidability-respecting* candidate has shipped
+  as `proofs/agda/EchoDecidable.agda` (`EchoDec f y = Dec (Echo f
+  y)` with six headline lemmas including `echo-dec-intro`,
+  `echo-dec-fin`, `echo-dec-compose-iso`; see `taxonomy.md` §8).
+  Follow-up: pick one of the remaining three refinements and
+  formalise.
 - **[unblocked]** Negative / co-echoes: formulate `CoEcho(f)` and its
   relationship to `Echo(f)`. Possibly resolves the quantitative /
   structural tension hinted at by `EchoTropical`.
-- **[unblocked]** 2-categorical shape: commit to a 2-category or
-  rule it out. Either answer unblocks the composition roadmap.
+- **[ruled out — see docs/echo-types/decisions/no-2-cat.adoc]**
+  2-categorical shape. Every would-be 2-cell in the landed code
+  is `refl` or forced trivial by propositionality (`≤g-prop`,
+  `⊑-prop`, `Echo-comp-iso` round-trips, pentagon projections,
+  `SliceHom`↔cone, `bridge-natural`); see
+  `decisions/no-2-cat.adoc` for the full verdict.
 - **[unblocked]** Presentation-dependence sub-theory: examples 5, 9,
   10 cluster here; write up the common pattern.
 - **[unblocked]** Gate 1 adjacency refresh: the five existing
