|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- EXPERIMENTAL — R2 deliverable (SHARED CARRIER). |
| 4 | +-- Carrier D : Grade → Set → Set for the echo-additive composition lines, |
| 5 | +-- PLUS the degrade reindexing action over the loss order extended to all of |
| 6 | +-- Grade, PLUS the carrier-level helpers the R3 laws consume (the fin 0 ≅ Id |
| 7 | +-- coercion, the D inf ≅ ⊤ collapse, the D-functor map, the ⊤-tower point). |
| 8 | +-- |
| 9 | +-- Imported by BOTH GradedMonad.agda (primary, φ) and GradedComonad.agda |
| 10 | +-- (secondary, δ). The two lines MUST NOT import each other; this module is |
| 11 | +-- their only shared dependency beyond Grade / Echo / stdlib (firewall W2). |
| 12 | +-- |
| 13 | +-- INVARIANTS (per STATE.adoc / DECISIONS.adoc D-2026-06-14-R1): |
| 14 | +-- --safe --without-K, zero postulates, no holes, no escape pragmas (W3/W4). |
| 15 | +-- No shipped module edited. Not imported by any shipped module (W5). |
| 16 | +-- NOT merged to main; experimental working-tree only (W6). |
| 17 | + |
| 18 | +module experimental.echo-additive.GradedCarrier where |
| 19 | + |
| 20 | +open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s) |
| 21 | +open import Data.Unit.Base using (⊤; tt) |
| 22 | +open import Data.Product.Base using (Σ; _,_; proj₁; proj₂; _×_) |
| 23 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) |
| 24 | + |
| 25 | +open import experimental.echo-additive.Grade |
| 26 | + using (Grade; fin; inf; _+g_) |
| 27 | + |
| 28 | +---------------------------------------------------------------------- |
| 29 | +-- R2 §1 — The carrier D : Grade → Set → Set |
| 30 | +-- |
| 31 | +-- Required endpoints (prompt + VarianceGate): |
| 32 | +-- D (fin 0) A = Id = A (Old.keep / no loss) |
| 33 | +-- D inf A = ⊤ (Old.forget / total collapse) |
| 34 | +-- D (fin (suc n)) A = ? (THE R2 QUESTION) |
| 35 | +-- |
| 36 | +-- ── Grounding in Echo / Echo-comp-iso ────────────────────────────── |
| 37 | +-- Echo-comp-iso (Echo.agda:73-96) is the bidirectional law |
| 38 | +-- Echo (g∘f) y ≅ Σ B (λ b → Echo f b × (g b ≡ y)). |
| 39 | +-- The COMBINING ("from") direction Echo-comp-iso-from FUSES an accumulated |
| 40 | +-- two-layer witness into one — this is the monadic μ the primary line φ |
| 41 | +-- builds on. The SPLITTING ("to") direction Echo-comp-iso-to SPLITS one |
| 42 | +-- layer into two — this is the comonadic δ the secondary line builds on. |
| 43 | +-- The nested RHS `Σ B (Echo f b × …)` is the shape of D r (D s A): an |
| 44 | +-- outer layer (the Σ-over-intermediate-base carrying a residue equation) |
| 45 | +-- wrapping an inner Echo. ONE additive grade-unit = ONE residue layer. |
| 46 | +-- |
| 47 | +-- ── THE R2 DESIGN CHOICE (the load-bearing honesty point) ────────── |
| 48 | +-- A residue layer of `Echo f b × (g b ≡ y)` needs a codomain map (`g`) |
| 49 | +-- and a base point (`y`) to pin a NON-TRIVIAL equation. The additive |
| 50 | +-- carrier has signature `Grade → Set → Set`: it receives a payload `A` |
| 51 | +-- and NOTHING ELSE — no codomain map, no base point. The only generic |
| 52 | +-- map available to instantiate Echo-comp-iso-{to,from} is `id`, and at |
| 53 | +-- `id`/`id` both the inner `Echo id b` (singleton at b) and the residue |
| 54 | +-- `id b ≡ y` (singleton at y) are CONTRACTIBLE. Hence every residue |
| 55 | +-- equation a finite additive layer could carry is `refl`-only, and the |
| 56 | +-- only K-free finite layer the carrier supports is PAYLOAD-INDEPENDENT — |
| 57 | +-- a `⊤` factor carrying the trivial residue. This is what makes the |
| 58 | +-- additive composition law DEFINITIONAL (D-fin-+-split below) and is the |
| 59 | +-- same fact that makes the additive grade STRUCTURALLY INERT: |
| 60 | +-- D (fin n) A ≅ A for every finite n. The grade counts layers; the layers |
| 61 | +-- carry no recoverable content because there is no codomain to recover |
| 62 | +-- against. This inertness is the carrier-side shadow of the R1 variance |
| 63 | +-- finding, and it is what both lines' law-discharge tests expose. |
| 64 | +-- |
| 65 | +-- The rejected alternative (recorded for honesty): a content-bearing |
| 66 | +-- finite layer `D-fin (suc n) A = Σ A (λ _ → D-fin n A)` — a real copy of |
| 67 | +-- A per layer — gives A^((m+1)(n+1)) under nesting, which does NOT fuse |
| 68 | +-- with addition's A^(n+m+1). The outer Σ would be over A vs over D-fin n A, |
| 69 | +-- so the additive split below would FAIL definitionally. Only the ⊤-padded |
| 70 | +-- tower fuses; making φ constructible via Echo-comp-iso-from forces it. |
| 71 | + |
| 72 | +-- Finite-grade carrier: n payload-independent residue layers over A. |
| 73 | +-- The trivial (refl-only) residue layer is written as a `⊤ ×` factor on |
| 74 | +-- the LEFT, so the additive split D-fin (m + n) A ≡ D-fin m (D-fin n A) |
| 75 | +-- is DEFINITIONAL. The δ line reads this LEFT-to-RIGHT (split, the |
| 76 | +-- additive image of Echo-comp-iso-TO); the φ line reads its `sym` |
| 77 | +-- RIGHT-to-LEFT (combine, the additive image of Echo-comp-iso-FROM). |
| 78 | +D-fin : ℕ → Set → Set |
| 79 | +D-fin zero A = A |
| 80 | +D-fin (suc n) A = ⊤ × D-fin n A |
| 81 | + |
| 82 | +-- Full carrier. |
| 83 | +D : Grade → Set → Set |
| 84 | +D (fin n) A = D-fin n A |
| 85 | +D inf A = ⊤ |
| 86 | + |
| 87 | +---------------------------------------------------------------------- |
| 88 | +-- R2 §2 — Endpoint sanity (all refl) |
| 89 | + |
| 90 | +D-fin0-Id : ∀ {A} → D (fin 0) A ≡ A |
| 91 | +D-fin0-Id = refl |
| 92 | + |
| 93 | +D-inf-Top : ∀ {A} → D inf A ≡ ⊤ |
| 94 | +D-inf-Top = refl |
| 95 | + |
| 96 | +-- The fin 0 ≅ Id coercion as named functions (definitional, so both refl). |
| 97 | +-- The R3 unit laws state "φ (fin 0) r = the D (fin 0)(−) ≅ Id coercion"; |
| 98 | +-- exposing the coercion by name lets that law be read against this carrier. |
| 99 | +D-fin0-coe : ∀ {A} → D (fin 0) A → A |
| 100 | +D-fin0-coe x = x |
| 101 | + |
| 102 | +D-fin0-coe-inv : ∀ {A} → A → D (fin 0) A |
| 103 | +D-fin0-coe-inv x = x |
| 104 | + |
| 105 | +-- The D inf ≅ ⊤ collapse, named for the same reason. |
| 106 | +D-inf-collapse : ∀ {A} → D inf A → ⊤ |
| 107 | +D-inf-collapse _ = tt |
| 108 | + |
| 109 | +---------------------------------------------------------------------- |
| 110 | +-- R2 §3 — Additive composition shape on FINITE grades |
| 111 | +-- |
| 112 | +-- The pivotal R2 lemma: on finite grades the additive carrier splits |
| 113 | +-- DEFINITIONALLY along +. D-fin (m + n) A ≡ D-fin m (D-fin n A) by a |
| 114 | +-- chain of refl, proved by induction on m. This is the carrier-level |
| 115 | +-- statement BOTH lines build their composition maps on top of, and is |
| 116 | +-- the additive shadow of Echo-comp-iso. |
| 117 | +-- |
| 118 | +-- The δ (secondary) line reads it LEFT-to-RIGHT (split: D (m+n) A → |
| 119 | +-- D m (D n A)); the φ (primary) line reads `sym` of it RIGHT-to-LEFT |
| 120 | +-- (combine: D m (D n A) → D (m+n) A). Both are transports along this same |
| 121 | +-- path — which is itself the symptom the variance finding predicts. |
| 122 | + |
| 123 | +D-fin-+-split : ∀ m n {A} → D-fin (m + n) A ≡ D-fin m (D-fin n A) |
| 124 | +D-fin-+-split zero n = refl |
| 125 | +D-fin-+-split (suc m) n {A} = cong (λ T → ⊤ × T) (D-fin-+-split m n) |
| 126 | + |
| 127 | +---------------------------------------------------------------------- |
| 128 | +-- R2 §4 — The carrier functor (D-fin-map / D-map) |
| 129 | +-- |
| 130 | +-- Needed to state D_r(φ_{s,t}) in the φ pentagon and D_r(δ_{s,t}) in the |
| 131 | +-- δ coassociativity. On the ⊤-padded carrier this is map-on-innermost- |
| 132 | +-- payload, leaving every trivial ⊤ layer fixed. Function-first argument |
| 133 | +-- order (matching the primary φ line's local convention). Hosted here so |
| 134 | +-- the carrier is self-describing; the line files keep their own local |
| 135 | +-- copies for their reasoning, but this is the canonical shared form. |
| 136 | + |
| 137 | +D-fin-map : ∀ {A B : Set} (f : A → B) (n : ℕ) → D-fin n A → D-fin n B |
| 138 | +D-fin-map f zero x = f x |
| 139 | +D-fin-map f (suc n) (tt , y) = tt , D-fin-map f n y |
| 140 | + |
| 141 | +D-map : ∀ {A B : Set} (f : A → B) (r : Grade) → D r A → D r B |
| 142 | +D-map f (fin n) x = D-fin-map f n x |
| 143 | +D-map f inf _ = tt |
| 144 | + |
| 145 | +-- Functor identity law (witness that D-map is a genuine functorial action). |
| 146 | +D-fin-map-id : ∀ {A : Set} (n : ℕ) (x : D-fin n A) → |
| 147 | + D-fin-map (λ a → a) n x ≡ x |
| 148 | +D-fin-map-id zero x = refl |
| 149 | +D-fin-map-id (suc n) (tt , y) = cong (λ z → tt , z) (D-fin-map-id n y) |
| 150 | + |
| 151 | +---------------------------------------------------------------------- |
| 152 | +-- R2 §5 — The ⊤-tower point |
| 153 | +-- |
| 154 | +-- Canonical inhabitant of any finite ⊤-padded carrier over ⊤. The δ line |
| 155 | +-- needs this to MANUFACTURE the m intermediate layers that total collapse |
| 156 | +-- (inf) destroyed when splitting D inf A = ⊤ into D (fin m) (D inf A) = |
| 157 | +-- D-fin m ⊤. Its inhabitedness is exactly carrier inertness — the |
| 158 | +-- carrier-side shadow of the variance finding on the δ side. |
| 159 | + |
| 160 | +D-fin-⊤-pt : ∀ m → D-fin m ⊤ |
| 161 | +D-fin-⊤-pt zero = tt |
| 162 | +D-fin-⊤-pt (suc m) = tt , D-fin-⊤-pt m |
| 163 | + |
| 164 | +---------------------------------------------------------------------- |
| 165 | +-- R2 §6 — The loss order on all of Grade, and the degrade reindexing |
| 166 | +-- action over it (fin 0 = Id unit; inf = Top collapse) |
| 167 | +-- |
| 168 | +-- The loss order ⊑g extends ℕ's ≤ with inf as the top (most lossy): |
| 169 | +-- fin m ⊑g fin n iff m ≤ n (losing MORE layers is higher) |
| 170 | +-- g ⊑g inf (total collapse is the cap) |
| 171 | +-- This is the same order whose 3-point restriction {fin 0, fin 1, inf} |
| 172 | +-- is the shipped EchoGraded `keep ≤g residue ≤g forget` action (read-only; |
| 173 | +-- mirrored here, NOT edited). fin 0 (no loss) is the bottom; inf the top. |
| 174 | + |
| 175 | +infix 4 _⊑g_ |
| 176 | +data _⊑g_ : Grade → Grade → Set where |
| 177 | + fin⊑fin : ∀ {m n} → m ≤ n → fin m ⊑g fin n |
| 178 | + ⊑inf : ∀ {g} → g ⊑g inf |
| 179 | + |
| 180 | +-- degrade: reindex a carrier value UP the loss order (forgetting structure). |
| 181 | +-- On the inert ⊤-tower, degrading fin m → fin n (m ≤ n) re-pads to n layers; |
| 182 | +-- degrading anything → inf collapses to tt. Total and K-free. |
| 183 | +-- |
| 184 | +-- The finite case recurses on the ≤ proof: the z≤n base re-pads a bare |
| 185 | +-- payload to n trivial layers (D-fin0-pad); the s≤s step peels one ⊤ on |
| 186 | +-- each side. |
| 187 | + |
| 188 | +-- pad a bare payload (D-fin 0 A = A) up to n trivial ⊤ layers. |
| 189 | +D-fin0-pad : ∀ {A} n → A → D-fin n A |
| 190 | +D-fin0-pad zero x = x |
| 191 | +D-fin0-pad (suc n) x = tt , D-fin0-pad n x |
| 192 | + |
| 193 | +degrade-fin : ∀ {A} {m n} → m ≤ n → D-fin m A → D-fin n A |
| 194 | +degrade-fin {n = n} z≤n x = D-fin0-pad n x |
| 195 | +degrade-fin (s≤s p) (tt , y) = tt , degrade-fin p y |
| 196 | + |
| 197 | +degrade : ∀ {A} {r s} → r ⊑g s → D r A → D s A |
| 198 | +degrade (fin⊑fin p) x = degrade-fin p x |
| 199 | +degrade ⊑inf _ = tt |
| 200 | + |
| 201 | +-- degrade at a reflexive finite step is the identity (the fin 0 unit law in |
| 202 | +-- carrier form: degrading along m ≤ m changes nothing). Witnessed via the |
| 203 | +-- ≤-reflexive proof built structurally. |
| 204 | +≤-refl-nat : ∀ n → n ≤ n |
| 205 | +≤-refl-nat zero = z≤n |
| 206 | +≤-refl-nat (suc n) = s≤s (≤-refl-nat n) |
| 207 | + |
| 208 | +degrade-fin-refl : ∀ {A} n (x : D-fin n A) → |
| 209 | + degrade-fin (≤-refl-nat n) x ≡ x |
| 210 | +degrade-fin-refl zero x = refl |
| 211 | +degrade-fin-refl (suc n) (tt , y) = cong (λ z → tt , z) (degrade-fin-refl n y) |
| 212 | + |
| 213 | +-- degrade into inf is the total collapse (the Old.forget endpoint, in |
| 214 | +-- carrier form): every value maps to the unique ⊤ inhabitant. |
| 215 | +degrade-to-inf : ∀ {A} {r} (p : r ⊑g inf) (x : D r A) → degrade p x ≡ tt |
| 216 | +degrade-to-inf ⊑inf x = refl |
0 commit comments