|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- EXPERIMENTAL — R4 deliverable: the F_r ⊣ U_r ADJUNCTION ATTEMPT on the |
| 4 | +-- CONTENT-FAITHFUL carrier (terminating-condition (ii) discriminator). |
| 5 | +-- |
| 6 | +-- Per STATE.adoc / DECISIONS.adoc: R2/R3 reached terminating condition (ii) |
| 7 | +-- (both the monad line φ and the comonad line δ discharge on the INERT |
| 8 | +-- carrier — but δ vacuously). Condition (ii) mandates a SEPARATE construction: |
| 9 | +-- build F_r and U_r as functors and ATTEMPT the adjunction F_r ⊣ U_r in |
| 10 | +-- --safe --without-K. The adjunction is NOT inherited from the R3 discharge. |
| 11 | +-- |
| 12 | +-- PREDICTION (GradedComonad §7 + VarianceGate §2 Option B): on the |
| 13 | +-- content-faithful carrier, F_r, U_r, the unit η, and the induced graded MONAD |
| 14 | +-- U_r F_r discharge; the COMONADIC half (the counit ε / the induced comonad |
| 15 | +-- F_r U_r comultiplication / the δ direction) is OBSTRUCTED — it forces a |
| 16 | +-- total map of shape ⊤ → Σ A (…) (invent a payload total collapse destroyed), |
| 17 | +-- which has NO K-free term. That obstruction is PARKED as an -- OBLIGATION |
| 18 | +-- comment (NEVER a postulate); the rest of the file typechecks clean. |
| 19 | +-- |
| 20 | +-- FIREWALL (W2): imports GradedCarrierFaithful + Grade + (read-only) Echo. |
| 21 | +-- Does NOT import GradedMonad / GradedComonad (their proofs are about the |
| 22 | +-- INERT carrier — a different object; importing them would contaminate the |
| 23 | +-- finding). ZERO POSTULATES, ZERO HOLES (W3/W4). NOT shipped (W5/W6). |
| 24 | + |
| 25 | +module experimental.echo-additive.GradedAdjunction where |
| 26 | + |
| 27 | +open import Data.Nat.Base using (ℕ; zero; suc) |
| 28 | +open import Data.Unit.Base using (⊤; tt) |
| 29 | +open import Data.Product.Base using (_,_) |
| 30 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) |
| 31 | + |
| 32 | +open import experimental.echo-additive.Grade |
| 33 | + using (Grade; fin; inf) |
| 34 | +open import experimental.echo-additive.GradedCarrierFaithful |
| 35 | + using (Dc; Dc-fin; Dc-map; Dc-fin-map) |
| 36 | + |
| 37 | +-- (Provenance note: the head-extraction counit ε and the diagonal unit η are |
| 38 | +-- the additive images of Echo-comp-iso-to/from — the split/combine directions |
| 39 | +-- in Echo.agda:73-96 — read on the content-faithful carrier. Echo itself is |
| 40 | +-- not imported here; the adjunction is built from the carrier functor alone, |
| 41 | +-- which is the standard unit/counit route and keeps the firewall minimal.) |
| 42 | + |
| 43 | +---------------------------------------------------------------------- |
| 44 | +-- R4 §1 — The functors F_r and U_r (VarianceGate §2 Option B, concretised) |
| 45 | +-- |
| 46 | +-- We work in the (only) category the additive signature gives us: SET, with |
| 47 | +-- F_r and U_r as endofunctors. The coeffect reading of Option B: |
| 48 | +-- |
| 49 | +-- F_r : Set → Set introduces r units of loss-structure. |
| 50 | +-- F_r A := Dc r A (the content-faithful r-layer tower over A). |
| 51 | +-- Functor action = Dc-map (maps over every layer). |
| 52 | +-- |
| 53 | +-- U_r : Set → Set FORGETS the loss-structure back to a bare payload. |
| 54 | +-- For the adjunction we take U_r = Id (the forgetful functor to the |
| 55 | +-- underlying Set), which is the standard coeffect choice: F_r is the |
| 56 | +-- "free r-graded" left adjoint, U_r the underlying-object right |
| 57 | +-- adjoint. (The grade is carried by F_r; U_r discards it.) |
| 58 | +-- |
| 59 | +-- The induced GRADED MONAD is U_r ∘ F_r = Dc r (the "store r layers" monad); |
| 60 | +-- the induced GRADED COMONAD is F_r ∘ U_r = Dc r as well (since U_r = Id), |
| 61 | +-- but read in the OPPOSITE variance. The asymmetry the variance finding |
| 62 | +-- predicts shows up in WHICH of unit / counit is K-free constructible. |
| 63 | + |
| 64 | +F : Grade → Set → Set |
| 65 | +F r A = Dc r A |
| 66 | + |
| 67 | +F-map : ∀ {A B : Set} (f : A → B) (r : Grade) → F r A → F r B |
| 68 | +F-map f r = Dc-map f r |
| 69 | + |
| 70 | +U : Set → Set |
| 71 | +U A = A |
| 72 | + |
| 73 | +U-map : ∀ {A B : Set} (f : A → B) → U A → U B |
| 74 | +U-map f = f |
| 75 | + |
| 76 | +---------------------------------------------------------------------- |
| 77 | +-- R4 §2 — THE UNIT η : A → U (F_r A) = Dc r A [EXPECTED: DISCHARGES] |
| 78 | +-- |
| 79 | +-- The unit of F_r ⊣ U_r at object A is a map A → U(F_r A) = Dc r A. It must |
| 80 | +-- introduce r layers of loss-structure from a bare payload. On the |
| 81 | +-- CONTENT-FAITHFUL carrier this is the diagonal: copy the payload into every |
| 82 | +-- one of the r+1 layers. NO invention — the payload is given, we duplicate it. |
| 83 | +-- This is the monadic-direction unit (Id ⇒ D) the variance finding flags as |
| 84 | +-- the natural, total direction. Total and K-free for every r. |
| 85 | + |
| 86 | +η-fin : ∀ (n : ℕ) {A} → A → Dc-fin n A |
| 87 | +η-fin zero a = a |
| 88 | +η-fin (suc n) a = a , η-fin n a |
| 89 | + |
| 90 | +η : ∀ (r : Grade) {A} → A → U (F r A) |
| 91 | +η (fin n) a = η-fin n a |
| 92 | +η inf a = tt -- Dc inf A = ⊤; collapse is forced (and total) |
| 93 | + |
| 94 | +-- The finite-grade head-EXTRACTION (the total fragment of the counit ε; the |
| 95 | +-- full counit and its obstruction are discussed in §4). Defined here because |
| 96 | +-- the monad multiplication μ (§3) is built from it. TOTAL and K-free: on the |
| 97 | +-- content-faithful carrier a finite layer genuinely HOLDS a payload, so we can |
| 98 | +-- read it off (proj₁ at suc; id at zero) — no invention. |
| 99 | +ε-fin : ∀ (n : ℕ) {A} → Dc-fin n A → A |
| 100 | +ε-fin zero x = x |
| 101 | +ε-fin (suc n) (a , _) = a |
| 102 | + |
| 103 | +---------------------------------------------------------------------- |
| 104 | +-- R4 §3 — THE COUNIT AS A NATURAL TRANSFORMATION, and the INDUCED MONAD μ |
| 105 | +-- |
| 106 | +-- The counit of F_r ⊣ U_r is a natural transformation ε_B : F U B → B, i.e. |
| 107 | +-- (since U = Id) ε_B : Dc r B → B, instantiated at EVERY object B. The |
| 108 | +-- induced monad U F_r = Dc r then has multiplication μ_A := U(ε_{F A}) = |
| 109 | +-- ε_{Dc r A} : Dc r (Dc r A) → Dc r A — i.e. μ is the SAME natural ε at the |
| 110 | +-- object Dc r A. This is the standard "monad-from-adjunction" recipe; it is |
| 111 | +-- NOT a free design choice. So once ε is fixed, μ is forced. |
| 112 | +-- |
| 113 | +-- ε_B = head-EXTRACTION (ε-fin at finite grade): on the content-faithful |
| 114 | +-- carrier a finite layer genuinely holds a payload, so we read off the head. |
| 115 | +-- TOTAL and K-free at finite grades. (At r = inf, ε_B : ⊤ → B is the |
| 116 | +-- obstruction — see §4.) |
| 117 | +-- |
| 118 | +-- Therefore μ_A = ε_{Dc r A} = head-extraction at object Dc r A: |
| 119 | + |
| 120 | +μ-fin : ∀ (n : ℕ) {A} → Dc-fin n (Dc-fin n A) → Dc-fin n A |
| 121 | +μ-fin n {A} = ε-fin n {Dc-fin n A} -- = U(ε_{F A}); FORCED by the recipe |
| 122 | + |
| 123 | +μ : ∀ (r : Grade) {A} → Dc r (Dc r A) → Dc r A |
| 124 | +μ (fin n) x = μ-fin n x |
| 125 | +μ inf _ = tt |
| 126 | + |
| 127 | +---------------------------------------------------------------------- |
| 128 | +-- R4 §4 — THE COUNIT ε : F_r (U A) → A = Dc r A → A [THE OBSTRUCTION POINT] |
| 129 | +-- |
| 130 | +-- The counit of F_r ⊣ U_r at object A is ε : F_r (U A) → A, i.e. Dc r A → A. |
| 131 | +-- It must EXTRACT a payload from an r-layer tower. Consider the two endpoints: |
| 132 | +-- |
| 133 | +-- r = fin 0 : Dc (fin 0) A = A, so ε = id. TOTAL, K-free. (extract at no loss) |
| 134 | +-- r = fin (suc n) : Dc-fin (suc n) A = Σ A (…), so ε = proj₁ (the head). |
| 135 | +-- TOTAL, K-free. (a content layer DOES hold a payload) |
| 136 | +-- r = inf : Dc inf A = ⊤. ε would need ⊤ → A. *** UNINHABITED *** |
| 137 | +-- total collapse destroyed every payload; there is no A to |
| 138 | +-- extract and no generic point. NO K-free total term. |
| 139 | +-- |
| 140 | +-- So ε is TOTAL on the finite grades (the content layers genuinely carry the |
| 141 | +-- payload — this is what content-faithfulness BUYS) but FAILS at r = inf. |
| 142 | +-- We expose the finite, total fragment (ε-fin, defined in §2 because μ uses it) |
| 143 | +-- and PARK the inf case as the obligation. |
| 144 | + |
| 145 | +-- The finite-grade counit. TOTAL and K-free. |
| 146 | +ε-fin-grade : ∀ (n : ℕ) {A} → F (fin n) (U A) → A |
| 147 | +ε-fin-grade n x = ε-fin n x |
| 148 | + |
| 149 | +-- OBLIGATION (R4 LIVE OBSTRUCTION — counit at inf, UNDISCHARGEABLE K-free): |
| 150 | +-- |
| 151 | +-- ε : ∀ (r : Grade) {A} → F r (U A) → A |
| 152 | +-- ε (fin n) x = ε-fin n x -- total: the head payload (extract) |
| 153 | +-- ε inf x = ? -- ⊤ → A, UNINHABITED for generic A. |
| 154 | +-- |
| 155 | +-- There is NO total K-free term completing the inf clause: x : ⊤ carries no |
| 156 | +-- payload, A has no generic point. A graded counit at the COLLAPSE grade would |
| 157 | +-- have to FABRICATE the payload total collapse destroyed — precisely the |
| 158 | +-- ⊤ → Σ A (…) shape GradedComonad §7 names (here in its starkest form ⊤ → A). |
| 159 | +-- This is the comonadic-direction invention the monad never needs. NOT |
| 160 | +-- postulated; parked. (The finite fragment ε-fin-grade above is the honest |
| 161 | +-- total content.) |
| 162 | + |
| 163 | +---------------------------------------------------------------------- |
| 164 | +-- R4 §5 — THE ADJUNCTION STATEMENT and the discharge attempt |
| 165 | +-- |
| 166 | +-- We state F_r ⊣ U_r via unit/counit + the two TRIANGLE (zig-zag) identities. |
| 167 | +-- With ε_B : Dc r B → B the natural counit and η_A : A → Dc r A the unit: |
| 168 | +-- |
| 169 | +-- (T1) ε_{F_r A} ∘ F_r(η_A) = id_{F_r A} : Dc r A → Dc r A |
| 170 | +-- F_r(η_A) = Dc-map η_A r : Dc r A → Dc r (Dc r A); ε_{F_r A} : Dc r (Dc r A) → Dc r A |
| 171 | +-- (T2) U_r(ε_A) ∘ η_{U_r A} = id_{U_r A} : A → A |
| 172 | +-- (U=Id) reads ε_A ∘ η_A = id_A : A → A. |
| 173 | +-- |
| 174 | +-- These are forced once η (diagonal copy) and ε (head extraction) are fixed: |
| 175 | +-- ε is the natural transformation, η is the unit, the recipe leaves no slack. |
| 176 | +-- |
| 177 | +-- ── (T2) DISCHARGES on FINITE grades (refl). ────────────────────────── |
| 178 | +-- ε_A ∘ η_A : at suc n, ε-fin (suc n) (η-fin (suc n) a) = proj₁ (a , η-fin n a) = a. |
| 179 | +triangle₂-fin : ∀ (n : ℕ) {A} (a : A) → ε-fin n (η-fin n a) ≡ a |
| 180 | +triangle₂-fin zero a = refl |
| 181 | +triangle₂-fin (suc n) a = refl |
| 182 | + |
| 183 | +-- (T2) at object Dc-fin n A is the monad LEFT-unit law μ ∘ η_{F A} = id; it is |
| 184 | +-- the same statement, instance of triangle₂-fin, and DISCHARGES (refl). |
| 185 | +monad-unit-left-fin : ∀ (n : ℕ) {A} (x : Dc-fin n A) → |
| 186 | + μ-fin n (η-fin n {Dc-fin n A} x) ≡ x |
| 187 | +monad-unit-left-fin zero x = refl |
| 188 | +monad-unit-left-fin (suc n) x = refl -- = triangle₂-fin (suc n) {Dc-fin n A} x |
| 189 | + |
| 190 | +-- ── (T1) is the OBSTRUCTION — it FAILS even at FINITE grades. ────────── |
| 191 | +-- (T1) ε_{F A} ∘ Dc-map η_A = id : Dc-fin n A → Dc-fin n A. |
| 192 | +-- At suc n with x = (a , xs): |
| 193 | +-- Dc-fin-map (η-fin (suc n)) (suc n) (a , xs) |
| 194 | +-- = (η-fin (suc n) a , Dc-fin-map (η-fin (suc n)) n xs) |
| 195 | +-- = ((a , η-fin n a) , …) |
| 196 | +-- ε_{F A} = ε-fin (suc n) extracts the head = (a , η-fin n a). |
| 197 | +-- The goal RHS is (a , xs). So (T1) demands η-fin n a ≡ xs for ARBITRARY xs. |
| 198 | +-- That is FALSE in general (η-fin n a is the all-a diagonal; xs is arbitrary). |
| 199 | +-- There is NO K-free term: the head-extraction counit DISCARDS the tail xs and |
| 200 | +-- the diagonal unit cannot have produced an arbitrary xs. This is the comonadic |
| 201 | +-- zig-zag failing: the counit, which must FORGET, cannot reconstruct the tail |
| 202 | +-- the unit's diagonal did not put there. PARKED, not postulated. |
| 203 | +-- |
| 204 | +-- OBLIGATION (R4 LIVE OBSTRUCTION — triangle T1, UNDISCHARGEABLE K-free): |
| 205 | +-- |
| 206 | +-- triangle₁-fin : ∀ (n : ℕ) {A} (x : Dc-fin n A) → |
| 207 | +-- ε-fin n (Dc-fin-map (η-fin n) n x) ≡ x |
| 208 | +-- triangle₁-fin zero x = refl -- base: id |
| 209 | +-- triangle₁-fin (suc n) (a , xs) = ? -- needs η-fin n a ≡ xs |
| 210 | +-- -- ?: goal (a , η-fin n a) ≡ (a , xs) reduces to η-fin n a ≡ xs, |
| 211 | +-- -- FALSE for arbitrary xs. No K-free (indeed NO) total inhabitant. |
| 212 | +-- |
| 213 | +-- The base case (n = 0) discharges (refl): at zero loss F U = Id and the |
| 214 | +-- triangle is trivial. EVERY positive content layer breaks it. This is sharper |
| 215 | +-- than the §4 inf-only prediction: content-faithfulness makes the comonadic |
| 216 | +-- zig-zag fail across ALL finite suc grades, because the counit must forget the |
| 217 | +-- per-layer content the diagonal unit duplicated, and forgetting is not |
| 218 | +-- invertible. The MONADIC half (η + μ = ε_{F A} with the LEFT unit law, |
| 219 | +-- monad-unit-left-fin) discharges; the comonadic zig-zag T1 does not. |
| 220 | + |
| 221 | +-- The base-case fragment of T1 (the only sub-case that discharges): |
| 222 | +triangle₁-fin-base : ∀ {A} (x : Dc-fin 0 A) → ε-fin 0 (Dc-fin-map (η-fin 0) 0 x) ≡ x |
| 223 | +triangle₁-fin-base x = refl |
| 224 | + |
| 225 | +---------------------------------------------------------------------- |
| 226 | +-- R4 §6 — The induced GRADED MONAD associativity-style law [DISCHARGES] |
| 227 | +-- |
| 228 | +-- The monad U F_r = Dc r with μ = ε_{F A} (head-extraction). The OTHER monad |
| 229 | +-- unit law (M-right) μ ∘ F(η) is exactly the failing T1 above — so as a MONAD |
| 230 | +-- the right-unit law also fails on this μ/η pairing at suc grades. What DOES |
| 231 | +-- discharge is the part of the structure that only ever projects/forgets: |
| 232 | +-- the left-unit (above) and the counit naturality on finite grades. |
| 233 | + |
| 234 | +-- Counit NATURALITY on finite grades: f ∘ ε = ε ∘ Dc-map f. [DISCHARGES] |
| 235 | +-- (ε is a natural transformation Dc r ⇒ Id on finite grades.) |
| 236 | +ε-natural-fin : ∀ (n : ℕ) {A B} (f : A → B) (x : Dc-fin n A) → |
| 237 | + f (ε-fin n x) ≡ ε-fin n (Dc-fin-map f n x) |
| 238 | +ε-natural-fin zero f x = refl |
| 239 | +ε-natural-fin (suc n) f (a , xs) = refl |
| 240 | + |
| 241 | +-- Unit NATURALITY on finite grades: Dc-map f ∘ η = η ∘ f. [DISCHARGES] |
| 242 | +η-natural-fin : ∀ (n : ℕ) {A B} (f : A → B) (a : A) → |
| 243 | + Dc-fin-map f n (η-fin n a) ≡ η-fin n (f a) |
| 244 | +η-natural-fin zero f a = refl |
| 245 | +η-natural-fin (suc n) f a = cong (λ z → f a , z) (η-natural-fin n f a) |
0 commit comments