|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- EchoKernel — the funext-free core of echo-types. |
| 4 | +-- |
| 5 | +-- This module is the *curated public surface* of the Echo foundation. |
| 6 | +-- Every other `Echo*` module in the tree transitively imports `Echo`; |
| 7 | +-- this re-export names that dependency-light core explicitly and pins |
| 8 | +-- the load-bearing lemma *types* so the kernel API cannot silently |
| 9 | +-- weaken without breaking this file's typecheck. |
| 10 | +-- |
| 11 | +-- Provenance / honesty (read before citing anything here): |
| 12 | +-- |
| 13 | +-- * `--safe --without-K`, zero postulates, zero escape pragmas. |
| 14 | +-- * The kernel's import cone is `Echo` + agda-stdlib only |
| 15 | +-- (`Level`, `Function.Base`, `Function.Bundles`, |
| 16 | +-- `Data.Product.Base`, `Relation.Binary.PropositionalEquality` |
| 17 | +-- [+ `.Properties`]). It contains *no* `Axiom.Extensionality` / |
| 18 | +-- funext anywhere — so every lemma re-exported below is |
| 19 | +-- funext-free, and this module's successful `--safe --without-K` |
| 20 | +-- build is itself the funext-free certificate. |
| 21 | +-- * The genuine funext-relativity in echo-types is the |
| 22 | +-- *pointwise-only* mediator property (`EchoPullback`, |
| 23 | +-- `echo-pullback-univ`), which lives strictly *outside* this |
| 24 | +-- kernel. The kernel deliberately keeps the cancel-iso |
| 25 | +-- round-trips first-order by taking the triangle identities |
| 26 | +-- (`triangle₁`, `triangle₂`) as explicit hypotheses rather than |
| 27 | +-- deriving them via funext. |
| 28 | +-- |
| 29 | +-- Non-claims (per `docs/retractions.adoc` R-2026-05-18, not |
| 30 | +-- un-retracted here): the kernel is a definitionally-grounded, |
| 31 | +-- loss-graded *reindexing* surface. It is *not* a graded comonad, it |
| 32 | +-- carries *no* universal/terminal property, and it is *not* a |
| 33 | +-- conservativity metatheorem. Nothing below asserts any of those. |
| 34 | +-- |
| 35 | +-- Kernel vs derived classification: see |
| 36 | +-- `docs/echo-types/echo-kernel-note.adoc` (one-page note, kept |
| 37 | +-- current in the same PR as this module). |
| 38 | + |
| 39 | +module EchoKernel where |
| 40 | + |
| 41 | +-- The whole funext-free core surface. Everything downstream that |
| 42 | +-- "imports Echo" is importing exactly this. |
| 43 | +open import Echo public |
| 44 | + |
| 45 | +------------------------------------------------------------------------ |
| 46 | +-- Kernel contract. |
| 47 | +-- |
| 48 | +-- The load-bearing lemmas the derived layer actually depends on, |
| 49 | +-- restated with explicit signatures and bound by definitional |
| 50 | +-- equality to the `Echo` proofs. This is a *contract*, not new |
| 51 | +-- mathematics: it forces the kernel's public types to remain exactly |
| 52 | +-- as documented, and re-checks each in the funext-free, |
| 53 | +-- extensionality-free, `--safe --without-K` cone. If any `Echo` |
| 54 | +-- lemma is weakened, generalised, or acquires a funext dependency, |
| 55 | +-- this section fails to typecheck. |
| 56 | +------------------------------------------------------------------------ |
| 57 | + |
| 58 | +module Kernel-contract where |
| 59 | + |
| 60 | + open import Level using (Level; _⊔_) |
| 61 | + open import Function.Base using (_∘_; id) |
| 62 | + open import Data.Product.Base using (Σ; _,_; _×_) |
| 63 | + open import Relation.Binary.PropositionalEquality |
| 64 | + using (_≡_; refl; sym; trans; cong) |
| 65 | + open import Function.Bundles using (_↔_) |
| 66 | + |
| 67 | + -- Echo functor: the structured remainder of an information-losing f. |
| 68 | + kernel-Echo : |
| 69 | + ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → B → Set (a ⊔ b) |
| 70 | + kernel-Echo = Echo |
| 71 | + |
| 72 | + -- Introduction into one's own fibre. |
| 73 | + kernel-echo-intro : |
| 74 | + ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (x : A) → Echo f (f x) |
| 75 | + kernel-echo-intro = echo-intro |
| 76 | + |
| 77 | + -- Fibrewise functorial action over a fixed base. |
| 78 | + kernel-map-over : |
| 79 | + ∀ {a a' b} {A : Set a} {A' : Set a'} {B : Set b} |
| 80 | + {f : A → B} {f' : A' → B} → |
| 81 | + MapOver f f' → ∀ {y : B} → Echo f y → Echo f' y |
| 82 | + kernel-map-over = map-over |
| 83 | + |
| 84 | + -- Functoriality: identity law. |
| 85 | + kernel-map-over-id : |
| 86 | + ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} (e : Echo f y) → |
| 87 | + map-over (id , (λ x → refl)) e ≡ e |
| 88 | + kernel-map-over-id = map-over-id |
| 89 | + |
| 90 | + -- Functoriality: composition law. |
| 91 | + kernel-map-over-comp : |
| 92 | + ∀ {a a' a'' b} |
| 93 | + {A : Set a} {A' : Set a'} {A'' : Set a''} {B : Set b} |
| 94 | + {f : A → B} {f' : A' → B} {f'' : A'' → B} |
| 95 | + (u1 : A → A') (c1 : ∀ x → f' (u1 x) ≡ f x) |
| 96 | + (u2 : A' → A'') (c2 : ∀ x → f'' (u2 x) ≡ f' x) |
| 97 | + {y : B} (e : Echo f y) → |
| 98 | + map-over {f = f} {f' = f''} |
| 99 | + (u2 ∘ u1 , (λ x → trans (c2 (u1 x)) (c1 x))) e |
| 100 | + ≡ map-over {f = f'} {f' = f''} (u2 , c2) |
| 101 | + (map-over {f = f} {f' = f'} (u1 , c1) e) |
| 102 | + kernel-map-over-comp = map-over-comp |
| 103 | + |
| 104 | + -- Composition accumulation iso (unconditional; closes the |
| 105 | + -- accumulation law of composition.md §1). |
| 106 | + kernel-Echo-comp-iso : |
| 107 | + ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} |
| 108 | + (f : A → B) (g : B → C) (y : C) → |
| 109 | + Echo (g ∘ f) y ↔ Σ B (λ b → Echo f b × (g b ≡ y)) |
| 110 | + kernel-Echo-comp-iso = Echo-comp-iso |
| 111 | + |
| 112 | + -- The single load-bearing path-algebra lemma. It is naturality of |
| 113 | + -- a homotopy `h : f ∼ id` along a path — first-order, funext-free. |
| 114 | + kernel-hom-natural-id : |
| 115 | + ∀ {a} {A : Set a} (f : A → A) (h : ∀ z → f z ≡ z) |
| 116 | + {x y : A} (p : x ≡ y) → |
| 117 | + trans (cong f p) (h y) ≡ trans (h x) p |
| 118 | + kernel-hom-natural-id = hom-natural-id |
| 119 | + |
| 120 | + -- Cancel iso, with the two triangle coherences kept as explicit |
| 121 | + -- hypotheses (this is *how* the kernel stays funext-free; funext |
| 122 | + -- would otherwise be needed to relate the two quasi-inverse laws). |
| 123 | + kernel-cancel-iso : |
| 124 | + ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} |
| 125 | + (f : A → B) (g : B → C) (s : C → B) |
| 126 | + (s-left : ∀ b → s (g b) ≡ b) |
| 127 | + (s-right : ∀ y → g (s y) ≡ y) |
| 128 | + (triangle₁ : ∀ b → cong g (s-left b) ≡ s-right (g b)) |
| 129 | + (triangle₂ : ∀ y → cong s (s-right y) ≡ s-left (s y)) |
| 130 | + (y : C) → |
| 131 | + Echo (g ∘ f) y ↔ Echo f (s y) |
| 132 | + kernel-cancel-iso = cancel-iso |
0 commit comments