|
| 1 | += Echo Types: A Definitionally-Grounded Graded Comonad of Structured Loss |
| 2 | +:toc: macro |
| 3 | +:toclevels: 3 |
| 4 | +:sectnums: |
| 5 | +:sectnumlevels: 3 |
| 6 | +:icons: font |
| 7 | + |
| 8 | +[IMPORTANT] |
| 9 | +==== |
| 10 | +*STATUS: living draft, not for submission.* Written 2026-05-17 while |
| 11 | +the formal result is fresh, so the narrative is captured at full |
| 12 | +strength now. Sections tagged *[EXPAND]* are deliberate stubs to be |
| 13 | +filled as more context accrues (broader worked examples, deeper |
| 14 | +related-work comparison, the ordinal/Buchholz consumer-evidence |
| 15 | +appendix, an evaluation section). Do not submit until the *[EXPAND]* |
| 16 | +tags are cleared and the venue/template are chosen (Pillar E logistics |
| 17 | +are offline/author-driven). The TYPES extended abstract |
| 18 | +(`types-abstract.adoc`) is the short, already-submission-ready |
| 19 | +companion; this is the full CPP/ITP-style mechanised-metatheory |
| 20 | +paper it grows into. |
| 21 | +==== |
| 22 | + |
| 23 | +toc::[] |
| 24 | + |
| 25 | +== Introduction |
| 26 | + |
| 27 | +Define, for `f : A → B` and `y : B`, |
| 28 | +`Echo f y := Σ (x : A) , (f x ≡ y)`. The central honesty of this work |
| 29 | +is that `Echo f y` is *definitionally* the homotopy fibre `fib f y` |
| 30 | +(HoTT book Def. 4.2.4): the bridge `echo↔fib` is mechanised with |
| 31 | +`refl` round-trips. We make this deflationary fact the foundation, |
| 32 | +not a footnote. |
| 33 | + |
| 34 | +The thesis of the paper is that the type-theoretic standing that |
| 35 | +*befits* echo is not the linear/dependent judgmental ladder — that |
| 36 | +comparison is a category error — but a **graded comonadic modality of |
| 37 | +structured loss** in the coeffect/quantitative lineage. The |
| 38 | +contribution is the full *characterisation package*, mechanised in |
| 39 | +Agda under `--safe --without-K` with zero postulates: a definitional |
| 40 | +identity, a universal property, a graded comonad whose laws provably |
| 41 | +reduce to order-propositionality, a separating model, model |
| 42 | +independence across two models, and a conservativity metatheorem — |
| 43 | +all under a falsifiable-gate methodology with a public retraction log. |
| 44 | + |
| 45 | +=== Why not "linear or dependent" |
| 46 | + |
| 47 | +Dependent types are a formation discipline (types depend on terms; |
| 48 | +LCCC / CwF semantics). Linear and substructural types are a |
| 49 | +structural-rule discipline (contraction/weakening restricted; |
| 50 | +symmetric monoidal closed / Benton's LNL semantics). Both change the |
| 51 | +judgmental apparatus. `Echo` introduces no new judgement, context |
| 52 | +structure, or formation rule — it is a derived Σ-type. Presenting |
| 53 | +bespoke "echo introduction/elimination rules" as primitive would be |
| 54 | +the fastest way to lose an informed reader. Owning "it is just `fib`" |
| 55 | +loudly pre-empts the reviewer's strongest objection and is the load |
| 56 | +the rest of the paper bears. |
| 57 | + |
| 58 | +=== Contributions |
| 59 | + |
| 60 | +. *Pinned identity.* `echo↔fib : Echo f y ↔ fiber f y`, |
| 61 | + definitional, `refl` round-trips (Pillar A). |
| 62 | +. *Universal property.* `Echo f y` as the pullback of `f` along the |
| 63 | + point `y : ⊤ → B`, with a funext-free, K-free terminal-cone |
| 64 | + property; a `SliceHom` *is* a cone (Pillar B-1, §3). |
| 65 | +. *Graded comonad.* counit / comultiplication over the loss-grade |
| 66 | + join-semilattice and all three laws — with the *H2 verdict* |
| 67 | + (§4.2): every law, coassociativity included, collapses to one |
| 68 | + path-independence lemma plus order-propositionality, with no path |
| 69 | + algebra (Pillar B-2). |
| 70 | +. *Separating model.* the graded model minus its single hypothesis |
| 71 | + `≤g-prop`: generic Σ-functoriality survives, the characteristic |
| 72 | + law is refuted at a decidable witness (Pillar C, §5). |
| 73 | +. *Model independence and conservativity.* an abstract model |
| 74 | + interface with the comonad laws proved once; two agreeing models; |
| 75 | + a conservativity metatheorem (Pillar D, §6). |
| 76 | +. *Methodology.* falsifiable gates with explicit retraction actions; |
| 77 | + one identity claim settled negatively and logged (§7). |
| 78 | + |
| 79 | +== Background and notation [EXPAND] |
| 80 | + |
| 81 | +Σ-types, the identity type, homotopy fibres, graded/coeffect |
| 82 | +comonads, the join-semilattice of loss grades. Agda `--safe |
| 83 | +--without-K` and what it excludes (K, univalence, funext). |
| 84 | + |
| 85 | +NOTE: *[EXPAND]* — flesh out with a self-contained primer on graded |
| 86 | +comonads (Petriček–Orchard–Mycroft; Brunel et al.; Atkey QTT; |
| 87 | +Orchard–Liepelt–Eades / Granule) and a one-paragraph HoTT-fibre |
| 88 | +recap, so the paper is readable by both the QTT and the HoTT |
| 89 | +communities without external lookup. |
| 90 | + |
| 91 | +== The universal property |
| 92 | + |
| 93 | +`Echo f y` is the pullback of `f : A → B` along the point |
| 94 | +`y : ⊤ → B`. The `⊤`-leg is forced, so a cone with apex `V` is |
| 95 | +exactly a map `p₁ : V → A` with `∀ v → f (p₁ v) ≡ y` — which *is* |
| 96 | +an `EchoCategorical.SliceHom (λ (_ : V) → y) f`; the bridge |
| 97 | +round-trips are `refl`. The terminal-cone property |
| 98 | +`echo-pullback-univ` gives existence (the obvious pairing) and |
| 99 | +*pointwise* uniqueness `∀ v → m' v ≡ m v` (not `m' ≡ m`, hence |
| 100 | +funext-free); the cone-morphism notion carries a witness-transport |
| 101 | +leg, which is what makes uniqueness provable without K (no UIP on |
| 102 | +`f a ≡ y` is assumed). This is the categorical-semantics anchor: a |
| 103 | +category theorist accepts echo as the limit of a cospan. |
| 104 | + |
| 105 | +== The graded comonad of structured loss |
| 106 | + |
| 107 | +=== Structure |
| 108 | + |
| 109 | +Over the loss-grade join-semilattice `(Grade, ⊔, keep)` with `keep` |
| 110 | +the bottom / monoidal unit: the counit `gextract` (zero-loss echo is |
| 111 | +the bare echo — the Pillar-A definitional move reused) and the |
| 112 | +comultiplication `gduplicate` (duplicating an observation splits the |
| 113 | +loss budget along the join, realised as the join-left embedding). |
| 114 | + |
| 115 | +[#h2-verdict] |
| 116 | +=== The H2 verdict (key technical insight) |
| 117 | + |
| 118 | +Stated in the *common-upper-bound idiom* — post-compose each |
| 119 | +(co)multiplication with the universal degrade into an *arbitrary* |
| 120 | +common grade, so both sides of every law land in the same object — |
| 121 | +the three graded-comonad laws (`gcomonad-counit-{l,r}`, |
| 122 | +`gcomonad-coassoc`) each collapse to exactly two ingredients: the |
| 123 | +path-independence lemma `degrade-compose` and propositionality of the |
| 124 | +loss order `≤g-prop`. There is no path algebra, no `subst`, no |
| 125 | +transport. The naive grade-equality phrasing of coassociativity would |
| 126 | +force a `subst` along `⊔`-associativity; the universal-arrow phrasing |
| 127 | +removes it entirely, because the join is a universal arrow and the |
| 128 | +order is a proposition. |
| 129 | + |
| 130 | +This is the paper's pivotal observation: the modality is *cheap* |
| 131 | +(no coherence tower) and, as §6 shows, *model-independent for the |
| 132 | +same reason* (the proof never inspects the carrier). |
| 133 | + |
| 134 | +== The separating model |
| 135 | + |
| 136 | +The separating model is the graded model with its *single* hypothesis |
| 137 | +`≤g-prop` deleted: a loss order with two distinct arrows `lo→hi` and |
| 138 | +a reindexing that distinguishes them. Generic Σ-functoriality |
| 139 | +(`map-over` id/comp) and the functorial unit still hold verbatim — it |
| 140 | +is a bona-fide Echo setting. The characteristic composition law is |
| 141 | +*refuted* at a concrete decidable witness, discharged by a checked |
| 142 | +`true ≢ false`. Conclusion: the loss law is not a generic |
| 143 | +Σ-consequence; it is carried *precisely* by order-propositionality. |
| 144 | +This is a positive countermodel object, extending the project's |
| 145 | +negative-exhibit discipline, and it answers the only objection every |
| 146 | +referee raises ("isn't this all Σ-lemmas with renamed components?") |
| 147 | +with a model rather than an argument. |
| 148 | + |
| 149 | +== Model independence and conservativity |
| 150 | + |
| 151 | +=== Two models, one structure |
| 152 | + |
| 153 | +An abstract interface `GradedLossModel` (a propositional grade order |
| 154 | +with a join and a composing reindexing) — exactly what the H2 verdict |
| 155 | +showed suffices. The graded-comonad laws are proved *once*, |
| 156 | +generically, from the interface (`GCLaws`); this *is* the |
| 157 | +model-independence theorem. Two instances: the Set/Type model |
| 158 | +(`EchoGraded`) and a relational model (`EchoStep`/`map-rel`, the |
| 159 | +composition law from `map-rel-comp` + `degrade-comp`). They agree |
| 160 | +under the graph = fibration bridge: `model-agreement` (carrier iso, |
| 161 | +round-trips `refl`) and `bridge-natural` (`map-over` ↔ `map-rel`). |
| 162 | +The graded comonad is the *same* structure in both. |
| 163 | + |
| 164 | +=== Conservativity |
| 165 | + |
| 166 | +Because `Echo = Σ` definitionally and the whole development is |
| 167 | +postulate-free under `--safe --without-K`, the loss modality is a |
| 168 | +*conservative, definitional* extension of MLTT+Σ: it adds structure |
| 169 | +(a characterised graded comonad) without adding strength. The |
| 170 | +metatheorem (`conservativity.adoc`) has a three-clause formal anchor: |
| 171 | +definitional (`EchoFiberBridge`), conservative (the postulate-free |
| 172 | +build, CI-enforced), modality-not-axiom (`EchoRelModel` / |
| 173 | +`EchoGradedComonad` / `EchoSeparating`). The conservativity argument |
| 174 | +is *operational* — discharged by the build itself. |
| 175 | + |
| 176 | +== Methodology: falsifiable gates and retraction |
| 177 | + |
| 178 | +Development is governed by gates (`roadmap-gates.adoc`) with explicit |
| 179 | +retraction actions and a public retraction log. One identity claim, |
| 180 | +the five-axis simultaneous-integration claim (EI-2), was settled |
| 181 | +*negatively* and is recorded as such; having cleanly killed it is |
| 182 | +part of the authority story, not a blemish. The funext boundary is |
| 183 | +real, known, and quarantined behind an isolated module |
| 184 | +(`examples/Transport.agda`, where `Field = Fin n → ℚ` forces funext); |
| 185 | +no result crosses it. We argue this discipline is itself a |
| 186 | +contribution: a template for honest mechanised-metatheory claims. |
| 187 | + |
| 188 | +== Evaluation and discussion [EXPAND] |
| 189 | + |
| 190 | +NOTE: *[EXPAND]* — proof-size / proof-cost table per pillar; what the |
| 191 | +common-upper-bound idiom buys versus the naive `subst` phrasing |
| 192 | +(quantified); a discussion of where the construction does *not* |
| 193 | +extend (the EI-2 negative result, the funext boundary) framed as |
| 194 | +strengths; threats to validity. |
| 195 | + |
| 196 | +== Related work [EXPAND] |
| 197 | + |
| 198 | +NOTE: *[EXPAND]* — detailed positioning against: Granule / QTT graded |
| 199 | +modalities; comonadic notions of computation (Uustalu–Vene); |
| 200 | +coeffects (Petriček–Orchard–Mycroft); HoTT fibrewise constructions; |
| 201 | +lens / optic literature (the witness-transport leg of |
| 202 | +`echo-pullback-univ` resembles the very-well-behaved-lens laws). Make |
| 203 | +the novelty crisp: not a new object, but a fully mechanised |
| 204 | +characterisation package with a falsifiable-gate methodology. |
| 205 | + |
| 206 | +== Conclusion |
| 207 | + |
| 208 | +Echo is the homotopy fibre equipped with a loss-grade lattice, |
| 209 | +forming a definitionally-grounded graded comonad of structured loss. |
| 210 | +Its standing comes not from being new but from being *characterised*: |
| 211 | +a universal property, a law-set that provably reduces to |
| 212 | +order-propositionality, a separating model, two agreeing models, and |
| 213 | +a mechanised conservativity metatheorem — with a falsifiable |
| 214 | +retraction discipline. The internal programme is complete; external |
| 215 | +validation is the remaining step. |
| 216 | + |
| 217 | +[appendix] |
| 218 | +== Ordinal / Buchholz consumer-evidence [EXPAND] |
| 219 | + |
| 220 | +NOTE: *[EXPAND]* — the ordinal-notation / Buchholz collapsing track |
| 221 | +is *consumer evidence* (an independent heavy user of the echo |
| 222 | +machinery), firewalled from the identity claim exactly as |
| 223 | +`roadmap.md` mandates. Summarise it here as an appendix only, with |
| 224 | +the firewall stated explicitly, once that track reaches its |
| 225 | +Bachmann–Howard milestone. |
| 226 | + |
| 227 | +[appendix] |
| 228 | +== Artefact statement |
| 229 | + |
| 230 | +Agda, stdlib 2.3, `--safe --without-K`, no postulates / no escape |
| 231 | +pragmas. Source `hyperpolymath/echo-types`; headline manifest |
| 232 | +`Smoke.agda`; plan `establishment-plan.adoc`; gates |
| 233 | +`roadmap-gates.adoc`; conservativity `conservativity.adoc`. Build: |
| 234 | +`agda -i proofs/agda proofs/agda/All.agda` then `Smoke.agda`, both |
| 235 | +exit 0. |
0 commit comments