Add phased Agda scope expansion, coherence bridges, and CI

Author: hyperpolymath

.github/workflows/agda.yml

@@ -0,0 +1,34 @@
+name: Agda
+
+on:
+  push:
+    branches:
+      - "**"
+  pull_request:
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install Agda and standard library
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y agda agda-stdlib
+
+      - name: Configure Agda standard library
+        run: |
+          STDLIB_LIB="$(find /usr/share -name 'standard-library.agda-lib' | head -n 1)"
+          if [ -z "$STDLIB_LIB" ]; then
+            echo "Could not locate standard-library.agda-lib"
+            exit 1
+          fi
+
+          mkdir -p "$HOME/.agda"
+          printf '%s\n' "$STDLIB_LIB" > "$HOME/.agda/libraries"
+          printf '%s\n' "standard-library" > "$HOME/.agda/defaults"
+
+      - name: Typecheck full suite
+        run: agda -i proofs/agda proofs/agda/All.agda

.gitignore

@@ -0,0 +1 @@
+*.agdai

README.md

@@ -0,0 +1,31 @@
+# echo-types
+
+Constructive Agda formalization of echo types / fibers:
+
+`Echo f y := Σ (x : A) , (f x ≡ y)`
+
+This repository provides a minimal, explicit development in ordinary intensional dependent type theory (`--safe --without-K`) with:
+
+- fiber introduction (`echo-intro`)
+- action on fibers over a fixed base (`map-over`)
+- identity law (`map-over-id`)
+- composition law (`map-over-comp`)
+- action along commuting squares (`map-square`)
+
+## Controlled Scope Broadening
+
+The formal scope is extended in controlled phases:
+
+- Phase A (`proofs/agda/EchoIndexed.agda`): role-indexed echoes `Echoᵢ` with trace-level witness separation.
+- Phase B (`proofs/agda/EchoEpistemicResidue.agda`): residue-based epistemic echoes `EchoR` with strict weakening/no-section results.
+- Phase C (`proofs/agda/EchoRelational.agda`): relational semantics `Step : S → O → Set` and output fibers `Σ s , Step s o`.
+- Phase D (`proofs/agda/EchoCategorical.agda`): slice/fibration packaging over the compiled deterministic and relational layers.
+
+## Build
+
+```bash
+cd /var/mnt/eclipse/repos/echo-types
+agda -i proofs/agda proofs/agda/Echo.agda
+agda -i proofs/agda proofs/agda/All.agda
+for f in proofs/agda/*.agda; do agda -i proofs/agda "$f"; done
+```

docs/assessment.adoc

@@ -0,0 +1,50 @@
+= Echo Types Assessment (M5)
+
+Date: 2026-04-18
+
+== Binary Conclusion
+
+*Established as distinct concept* (within the current formal scope of this repository).
+
+== Basis for Verdict
+
+The roadmap required three independent criteria for identity beyond raw sigma/fiber syntax.
+All three are currently met.
+
+=== 1. Distinct phenomenon isolated
+
+Target phenomenon: *structured loss under non-injective computation*.
+
+Evidence:
+
+* `collapse-non-injective` and `no-section-collapse` in `proofs/agda/EchoCharacteristic.agda`
+* `no-section-visible` in `proofs/agda/EchoCharacteristic.agda`
+
+These show outputs can be operationally irreversible while the echo layer remains proof-relevant.
+
+=== 2. Characteristic theorem family exists
+
+Evidence in `proofs/agda/Echo.agda`, `proofs/agda/EchoCharacteristic.agda`,
+and `proofs/agda/EchoResidue.agda`:
+
+* echo introduction and transport laws (`echo-intro`, `map-over`, `map-over-id`, `map-over-comp`, `map-square`)
+* distinct echoes over same visible value (`echo-true≢echo-false`, `stateA≢stateB`)
+* strict weakening to residue plus non-recoverability (`strict-weakening-collapse`, `no-section-collapse-to-residue`)
+
+This is more than definitional unpacking: it exhibits irreversible-but-not-forgetful behavior.
+
+=== 3. Canonical examples succeed
+
+Evidence in `proofs/agda/EchoExamples.agda`:
+
+* sign-loss squaring model (`square9`)
+* structured projection with forgotten component (`visible`)
+* quotient/collapse representative class behavior (`quot`)
+* residue identification under collapse (`collapse-residue-identifies`)
+
+These examples are compiled Agda objects/lemmas, not prose-only claims.
+
+== Scope Note
+
+This verdict is about proof-theoretic identity in ordinary intensional DTT (`--safe --without-K`) as developed here.
+It does not claim a completed full categorical semantics formalization yet.

echo-types.agda-lib

@@ -0,0 +1,3 @@
+name: echo-types
+include: proofs/agda
+depend: standard-library

proofs/agda/All.agda

@@ -0,0 +1,20 @@
+{-# OPTIONS --safe --without-K #-}
+
+module All where
+
+open import Echo
+open import EchoCharacteristic
+open import EchoResidue
+open import EchoExamples
+
+open import EchoChoreo
+open import EchoEpistemic
+open import EchoLinear
+open import EchoGraded
+open import EchoTropical
+
+open import EchoIndexed
+open import EchoEpistemicResidue
+open import EchoRelational
+open import EchoCategorical
+open import EchoScope

proofs/agda/Echo.agda

@@ -0,0 +1,65 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Echo where
+
+open import Level using (Level; _⊔_)
+open import Function.Base using (_∘_; id)
+open import Data.Product.Base using (Σ; _,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; cong)
+
+-- Echo_f(y) := Σ (x : A) , (f x ≡ y)
+Echo : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → B → Set (a ⊔ b)
+Echo {A = A} f y = Σ A (λ x → f x ≡ y)
+
+-- Introduction into own fiber.
+echo-intro : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (x : A) → Echo f (f x)
+echo-intro f x = x , refl
+
+-- Morphisms over a fixed codomain B.
+MapOver :
+  ∀ {a a' b} {A : Set a} {A' : Set a'} {B : Set b} →
+  (f : A → B) → (f' : A' → B) → Set (a ⊔ a' ⊔ b)
+MapOver {A = A} {A' = A'} f f' = Σ (A → A') (λ u → ∀ x → f' (u x) ≡ f x)
+
+-- Action on fibers over fixed base B.
+map-over :
+  ∀ {a a' b} {A : Set a} {A' : Set a'} {B : Set b}
+  {f : A → B} {f' : A' → B} →
+  MapOver f f' → ∀ {y : B} → Echo f y → Echo f' y
+map-over (u , commute) (x , p) = u x , trans (commute x) p
+
+-- Identity law (pointwise on each fiber element).
+map-over-id :
+  ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} (e : Echo f y) →
+  map-over (id , (λ x → refl)) e ≡ e
+map-over-id (x , p) = refl
+
+trans-assoc :
+  ∀ {a} {A : Set a} {x y z w : A}
+  (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) →
+  trans (trans p q) r ≡ trans p (trans q r)
+trans-assoc refl q r = refl
+
+-- Composition law (pointwise on each fiber element).
+map-over-comp :
+  ∀ {a a' a'' b}
+  {A : Set a} {A' : Set a'} {A'' : Set a''} {B : Set b}
+  {f : A → B} {f' : A' → B} {f'' : A'' → B}
+  (u1 : A → A') (c1 : ∀ x → f' (u1 x) ≡ f x)
+  (u2 : A' → A'') (c2 : ∀ x → f'' (u2 x) ≡ f' x)
+  {y : B} (e : Echo f y) →
+  map-over {f = f} {f' = f''}
+    (u2 ∘ u1 , (λ x → trans (c2 (u1 x)) (c1 x))) e
+  ≡ map-over {f = f'} {f' = f''} (u2 , c2)
+      (map-over {f = f} {f' = f'} (u1 , c1) e)
+map-over-comp u1 c1 u2 c2 (x , p)
+  rewrite trans-assoc (c2 (u1 x)) (c1 x) p = refl
+
+-- Action along a commuting square: f' ∘ u = v ∘ f.
+map-square :
+  ∀ {a a' b b'}
+  {A : Set a} {A' : Set a'} {B : Set b} {B' : Set b'}
+  (f : A → B) (f' : A' → B') (u : A → A') (v : B → B')
+  (square : ∀ x → f' (u x) ≡ v (f x)) {y : B} →
+  Echo f y → Echo f' (v y)
+map-square f f' u v square (x , p) = u x , trans (square x) (cong v p)

proofs/agda/EchoCategorical.agda

@@ -0,0 +1,124 @@
+{-# OPTIONS --safe --without-K #-}
+
+module EchoCategorical where
+
+open import Echo
+open import EchoRelational using (EchoStep; RelMap; map-rel; map-rel-id; map-rel-comp)
+
+open import Level using (Level; _⊔_)
+open import Function.Base using (id; _∘_)
+open import Data.Product.Base using (Σ; _,_; proj₁)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; subst)
+
+-- Phase D (part 1): slice-style packaging for deterministic maps.
+record SliceHom
+  {a a' b} {A : Set a} {A' : Set a'} {B : Set b}
+  (f : A → B) (f' : A' → B) : Set (a ⊔ a' ⊔ b) where
+  field
+    arrow : A → A'
+    commute : ∀ x → f' (arrow x) ≡ f x
+
+open SliceHom public
+
+slice-to-mapover :
+  ∀ {a a' b} {A : Set a} {A' : Set a'} {B : Set b}
+  {f : A → B} {f' : A' → B} →
+  SliceHom f f' → MapOver f f'
+slice-to-mapover h = arrow h , commute h
+
+mapover-to-slice :
+  ∀ {a a' b} {A : Set a} {A' : Set a'} {B : Set b}
+  {f : A → B} {f' : A' → B} →
+  MapOver f f' → SliceHom f f'
+mapover-to-slice (u , c) = record { arrow = u ; commute = c }
+
+slice-id :
+  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) →
+  SliceHom f f
+slice-id f = record
+  { arrow = id
+  ; commute = λ _ → refl
+  }
+
+slice-comp :
+  ∀ {a a' a'' b}
+  {A : Set a} {A' : Set a'} {A'' : Set a''} {B : Set b}
+  {f : A → B} {f' : A' → B} {f'' : A'' → B} →
+  SliceHom f f' → SliceHom f' f'' → SliceHom f f''
+slice-comp h₁ h₂ = record
+  { arrow = arrow h₂ ∘ arrow h₁
+  ; commute = λ x → trans (commute h₂ (arrow h₁ x)) (commute h₁ x)
+  }
+
+slice-act :
+  ∀ {a a' b} {A : Set a} {A' : Set a'} {B : Set b}
+  {f : A → B} {f' : A' → B} →
+  SliceHom f f' → ∀ {y : B} → Echo f y → Echo f' y
+slice-act h = map-over (slice-to-mapover h)
+
+slice-act-id :
+  ∀ {a b} {A : Set a} {B : Set b}
+  {f : A → B} {y : B} (e : Echo f y) →
+  slice-act (slice-id f) e ≡ e
+slice-act-id = map-over-id
+
+slice-act-comp :
+  ∀ {a a' a'' b}
+  {A : Set a} {A' : Set a'} {A'' : Set a''} {B : Set b}
+  {f : A → B} {f' : A' → B} {f'' : A'' → B}
+  (h₁ : SliceHom f f') (h₂ : SliceHom f' f'')
+  {y : B} (e : Echo f y) →
+  slice-act (slice-comp h₁ h₂) e ≡
+  slice-act h₂ (slice-act h₁ e)
+slice-act-comp h₁ h₂ = map-over-comp (arrow h₁) (commute h₁) (arrow h₂) (commute h₂)
+
+-- Phase D (part 2): fibration-style packaging for relational semantics.
+module Fibration {s o r} {S : Set s} {O : Set o} (Step : S → O → Set r) where
+
+  Fiber : O → Set (s ⊔ r)
+  Fiber = EchoStep Step
+
+  Total : Set (s ⊔ o ⊔ r)
+  Total = Σ O Fiber
+
+  π : Total → O
+  π = proj₁
+
+  fiber-to-echo :
+    ∀ {out : O} → Fiber out → Echo π out
+  fiber-to-echo {out} e = (out , e) , refl
+
+  echo-to-fiber :
+    ∀ {out : O} → Echo π out → Fiber out
+  echo-to-fiber ((out' , e) , p) = subst Fiber p e
+
+  echo-to-fiber∘fiber-to-echo :
+    ∀ {out : O} (e : Fiber out) →
+    echo-to-fiber (fiber-to-echo e) ≡ e
+  echo-to-fiber∘fiber-to-echo e = refl
+
+  fiber-map :
+    ∀ {s' r'} {S' : Set s'} {Step' : S' → O → Set r'} →
+    RelMap Step Step' → ∀ {out : O} → Fiber out → EchoStep Step' out
+  fiber-map = map-rel
+
+  fiber-map-id :
+    ∀ {out : O} (e : Fiber out) →
+    fiber-map (id , (λ {st} {out} p → p)) e ≡ e
+  fiber-map-id e = map-rel-id {Step = Step} e
+
+  rel-fiber-map-comp :
+    ∀ {s' s'' r' r''}
+    {S' : Set s'} {S'' : Set s''}
+    {Step' : S' → O → Set r'}
+    {Step'' : S'' → O → Set r''}
+    (u₁ : S → S') (pres₁ : ∀ {st out} → Step st out → Step' (u₁ st) out)
+    (u₂ : S' → S'') (pres₂ : ∀ {st out} → Step' st out → Step'' (u₂ st) out)
+    {out : O} (e : Fiber out) →
+    map-rel {Step = Step} {Step' = Step''}
+      (u₂ ∘ u₁ , λ p → pres₂ (pres₁ p)) e
+    ≡ map-rel {Step = Step'} {Step' = Step''} (u₂ , pres₂)
+        (map-rel {Step = Step} {Step' = Step'} (u₁ , pres₁) e)
+  rel-fiber-map-comp {Step' = Step'} {Step'' = Step''} u₁ pres₁ u₂ pres₂ e =
+    map-rel-comp {Step = Step} {Step' = Step'} {Step'' = Step''}
+      u₁ pres₁ u₂ pres₂ e