Per-neighbour distinctness comparisons for the gate #1 identity
claim. This directory is the artefact roadmap-gates.adoc § Gate 1
specifies. It supersedes the consolidated neighbour-theory section
in docs/gate-1-distinct-phenomenon.adoc, which now points here.
The exploration that motivated this directory (and identified the
gaps it fills) is in docs/integration-audit.adoc § "Adjacency
exploration".
Working through the neighbours individually surfaced a structural observation that the consolidated framing was glossing: the distinctness arguments fall into two structurally different families.
Echo wins by carrying type-data where the neighbour carries
propositional or single-witness content. The formal certificate
is the family of echo-not-prop lemmas formalised in
proofs/agda/examples/:
-
TropicalArgmin.echo-not-prop— three paths, two argmins -
EpistemicUpdate.echo-not-prop— eight worlds, four consistent -
LinearErasure.echo-not-prop— two annotated types, one erasure
The general theorem (Q2.1 in next-questions.adoc): for
non-injective f : A → B with at least two distinct preimages of
y, is-prop (Echo f y) → ⊥. Proved. The received-y form is
EchoTruncation.echo-not-prop, re-exported as
characteristic.NonTruncatable.Q2-1; the stronger constructed-y
form (non-injectivity of f forces a non-propositional fibre,
the y being produced rather than assumed) is
characteristic.NonTruncatable.non-injective⇒echo-not-prop. The
gate-2 audit (recorded in that module’s header and in
next-questions.adoc §Q2.1) demotes the received-y form as
Σ-reducible and forwards only the constructed-y form as a
candidate nominee.
Truncation arguments are load-bearing against:
-
Refinement types (in propositional-predicate variants like F\*, Liquid Haskell — see
refinement-types.adoc) -
Information-flow non-interference (in relational variants — see
information-flow.adoc) -
Provenance (in single-witness variants — see
provenance.adoc) -
Quotient types (which collapse witnesses by construction — see
quotients.adoc)
Echo wins because the natural 2-cell in the neighbour’s framework is Σ-over-preimages-shaped, i.e., already echo-shaped, when incomparable kernels force a true 2-cell rather than a refinement map. The formal certificates:
-
EchoVsQuotient.Sophisticated.equalizer→echo-pair— quotients' 2-categorical encoding’s natural 2-cell is the equalizer of two parallel maps, which IS Σ-over-preimages. -
EchoVsGalois.Sophisticated.meet→echo-intersection— abstract interpretation’s natural 2-cell is the meet in the abstraction lattice, which IS Σ-over-preimages with a paired predicate.
Both arguments are sealed against subordinate sub-cases: joins
(Joins.join-universal), indexed families with coherence laws
(IndexedFamilies.s-2-reduction).
The diagonal correspondence
(Sophisticated.meet-on-diagonal→equalizer) establishes that the
two arguments agree where they overlap: the AI meet specialises to
the quotient equalizer when output values coincide.
2-cell arguments are load-bearing against:
-
Quotient types (
quotients.adoc) -
Galois connections / abstract interpretation (
galois-connections.adoc)
A subset of the truncation family worth distinguishing: provenance
specifically tracks one source per output rather than truncating
to "some source exists". The win is at non-injective points; the
loss is the same echo-not-prop-flavoured certificate but the
neighbour’s failure mode is "single-witness selection" rather than
"propositional truncation" per se.
Treated under truncation in provenance.adoc, with the
multiplicity-vs-truncation distinction noted explicitly.
| Neighbour | Truncation | 2-cell | Notes |
|---|---|---|---|
Refinement types |
Wins against propositional-predicate variants ( |
N/A |
Tied with Σ-relevant variants (Agda, Coq) — these are echo |
Quotient types |
Wins (quotients collapse witnesses by construction) |
Wins ( |
Strongest case; argued on both axes |
Galois / AI |
Partial (Galois is propositional/relational about the abstract domain) |
Wins ( |
Diagonal correspondence with quotients |
IFC (Goguen-Meseguer) |
Wins against relational variants ( |
Open question against type-theoretic IFC variants |
Genuine open work — see Q2.x candidates |
Provenance |
Wins against single-witness variants (multiplicity) |
Wins (transitive provenance reduces to S-2 case) |
Multiplicity wording is sharper than truncation here |
Modal type theories (QTT, etc.) |
Wins against propositional-mode accounts |
N/A (modal type theories make 2-cells syntactic primitives) |
Co-extensive with QTT-class systems on bare echo; integration recipe is open |
HoTT fibers |
N/A (HoTT fibers are echo by another name) |
N/A (cubical 2-cells are equalizers definitionally) |
Tied; the win is over the propositional-truncation modality, not over HoTT |
|
Note
|
EI-2 cascade. The 2-cell wins above hold on their own structural
terms (equalizers and meets are Σ-over-preimages-shaped). The
recipe-level cross-axis commutations on 2D and 3D products are a
different story: per the EI-2 investigation
( Concretely: across seven data points (sibling 2D constructions
In short: the integration recipe does not carry the distinctness load. The 2-cell argument and the truncation argument do, and they stand independently.
|
The neighbour-theory section in
gate-1-distinct-phenomenon.adoc previously listed five neighbours
in a single doc. That section is now superseded by this directory.
The consolidated doc retains the integration-flavoured argument
and the falsification tests T1/T2/T3, but for per-neighbour
comparison work it points here.
The split is per roadmap-gates.adoc § Gate 1, which originally
specified docs/adjacency/ as the gate-1 artefact. The
consolidated form was a transitional state during parallel work;
this directory is the intended structure.
| File | Neighbour |
|---|---|
|
Quotient types / setoid quotients |
|
Setoid quotients (extrinsic, named-relation variant) |
|
Galois connections / abstract interpretation |
|
Refinement types (Σ-relevant and propositional variants) |
|
Information-flow non-interference (Goguen-Meseguer lineage) |
|
Provenance / data lineage |
|
K-provenance (Green-Karvounarakis-Tannen semirings) |
|
QTT, Reed-Pfenning modal calculi, adjoint modalities |
|
HoTT homotopy fibers (cubical and Book HoTT) |
|
Cubical Agda, RedPRL, redtt, cooltt |
|
Lenses, prisms, profunctor optics |
|
Meta: doc-surgery instructions for |
|
Meta: this file (index + argument families + axis-coverage matrix) |
Cross-reference of each adjacency note against the 8 taxonomy axes
defined in docs/echo-types/taxonomy.md. Refreshed 2026-05-20 — most
notes predate axis 8 (added with the EchoDecidable/EchoFiberCount
landings) and therefore do not currently engage it; the open ○
markings below flag where axis-8 implications exist but are not
formally argued.
Legend: ● primary axis (load-bearing in the note’s distinctness claim); ○ axis-8 implication exists but is open / post-dates the note; — axis not engaged.
| Note | 1 Ext/Int | 2 Exact/Approx | 3 Loc/Glob | 4 Canon/Pres | 5 Comp/Non | 6 Stat/Dyn | 7 PR/PI | 8 IT/Comp |
|---|---|---|---|---|---|---|---|---|
cubical-systems |
● |
— |
— |
● |
— |
— |
● |
— |
galois-connections |
— |
— |
— |
— |
● |
— |
● |
— |
hott-fibers |
● |
— |
— |
— |
— |
— |
● |
— |
information-flow |
— |
— |
— |
— |
— |
● |
● |
○ |
lenses-and-optics |
— |
— |
— |
● |
● |
— |
● |
— |
modal-type-theories |
— |
— |
— |
— |
● |
— |
● |
○ |
provenance |
— |
— |
— |
— |
— |
— |
● |
— |
provenance-semirings |
— |
— |
— |
— |
● |
— |
● |
○ |
quotients |
● |
— |
— |
— |
● |
— |
● |
— |
refinement-types |
— |
— |
— |
— |
— |
— |
● |
— |
setoid-quotients |
● |
— |
— |
● |
— |
— |
● |
— |
-
Axis 7 (proof-relevant vs proof-irrelevant) is universal. Every one of the 11 substantive notes routes its distinctness through axis 7. This is the "truncation argument" family’s load-bearing axis — the formal certificate is
echo-not-prop. -
Axis 5 (compositional vs non-compositional) carries the 2-cell argument. Galois, quotients, modal-type-theories, lenses-and- optics, provenance-semirings all engage axis 5 — these are the notes whose distinctness arguments route through composition structure (
EchoCategorical, the per-decoration composition sweep, theEcho-comp-isopentagon). -
Axis 1 (extensional vs intensional) shows up in four notes — the ones contrasting echo’s intensional-witness stance against a neighbour’s extensional / propositional collapse (cubical, hott-fibers, quotients, setoid-quotients).
-
Axis 4 (canonical vs presentation-dependent) picks up three notes — cubical (equality choice), lenses-and-optics (get/put split), setoid-quotients (named equivalence vs implicit kernel).
-
Axes with no neighbour coverage — see §"Gaps" below.
-
Axis 2 (exact vs approximate) has no adjacency note. The axis-2 artifact is
EchoApprox.agda(parametric pseudo-metric, three headline lemmas); its closest neighbour analogue — e.g. metric category theory, V-categories, weighted limits — is unwritten. Candidate future note:metric-categories.adoc. -
Axis 3 (local vs global) has no adjacency note. The closest candidates are sheaf-theoretic / local-trivialisation framings; not yet written.
-
Axis 6 (static vs dynamic) has only one note (
information- flow, via knowledge update). Other dynamic-typing or temporal neighbours (reactive / temporal logic / coalgebraic process theory) are unwritten. -
Axis 8 (information-theoretic vs computational access) has no formal neighbour treatment. Three notes have open implications, flagged ○ above:
-
information-flow.adoc— cryptographic threat models route through axis 8 when low observers are computationally bounded. Not addressed in the current relational framing. -
modal-type-theories.adoc— QTT-style quantitative annotations are proxies for resource control (taxonomy §"Axis 8" lines 236–238) but are not full computational-access tracking. The note treats QTT as a decoration neighbour (axis 5/7), not an axis-8 neighbour. -
provenance-semirings.adoc— K-semirings with a cost-tracking interpretation (e.g. tropical(min, +)-semirings) would engage axis 8. The current note treats K-provenance as a decoration neighbour (axis 5/7).Candidate future notes that *would* directly engage axis 8: `cryptographic-one-way-functions.adoc` (witness inhabitedness vs poly-time witness extraction); `cost-monads.adoc` (resource monads à la Hindley-Milner with cost effects); `complexity-classes -as-modalities.adoc` (P/NP/PSPACE as access modalities).
-
None of the 11 substantive notes' verdicts is incorrect against the current taxonomy. Three notes carry framings that would benefit from explicit axis-8 disclaimers (the three ○ rows). No note’s distinctness claim is invalidated by the post-hoc addition of axis 8; the omission is one of coverage, not contradiction.
The INSERTION_NOTE.adoc describes a doc-surgery operation. As a
meta-note it has no axis engagement; retained for traceability.
The truncation argument has formal exhibits for three of its
target neighbours via gate-3’s echo-not-prop family
(TropicalArgmin, EpistemicUpdate, LinearErasure). The
general theorem (Q2.1) is now stated and proved in
characteristic.NonTruncatable (received-y form Q2-1 plus the
stronger constructed-y form non-injective⇒echo-not-prop),
discharging the truncation argument against all four
truncation-vulnerable neighbours at the general level rather than
the three n=2 instances. The remaining open work is the gate-2
nomination decision (the audit demotes the received-y form as
Σ-reducible and forwards only the constructed-y form), not the
formalisation.
The 2-cell argument has formal exhibits for both of its target
neighbours (quotients via EchoVsQuotient.Sophisticated, Galois
via EchoVsGalois.Sophisticated).
The remaining neighbours (IFC, provenance, modal type theories, HoTT fibers) have prose adjacency notes here but no dedicated Agda formalisation. Each note states what would be required for formalisation and forwards the obligation to either Q2.x (for recipe-level distinctness from a given neighbour) or to Q3.x (for a canonical example exercising the distinctness).
The honest summary: gate #1 has a strong consolidated argument plus formalised obstructions against the two strongest neighbours (quotients, Galois) plus formalised truncation wins on three domains (tropical, epistemic, linear). The remaining neighbours have framed but unformalised distinctness claims.