Merge branch 'main' into claude/echo-types-theory-docs

Author: hyperpolymath

proofs/agda/All.agda

@@ -22,6 +22,10 @@ open import EchoCategorical
 open import EchoScope
 open import EchoOrdinal
 open import EchoJanusBridge
+open import Dyadic
+open import DyadicEchoBridge
+open import EchoThermodynamics
+open import EchoStabilityTests
 
 open import Ordinal.Base
 open import Ordinal.Closure
@@ -30,6 +34,7 @@ open import Ordinal.PsiSimple
 open import Ordinal.OmegaMarkers
 open import Ordinal.Buchholz.Syntax
 open import Ordinal.Buchholz.Closure
+open import Ordinal.Buchholz.Order
 open import Ordinal.Buchholz.Psi
 open import Ordinal.Buchholz.Examples
 open import Ordinal.Buchholz.WellFormed

proofs/agda/DyadicEchoBridge.agda

@@ -26,19 +26,25 @@ SessionAsFunction {p} (Select S1 S2) q = SessionAsFunction S1 q ⊎ SessionAsFun
 -- Simplified echo over session types (avoiding universe issues)
 SessionEcho : ∀ {p} → (q : Party) → Session p → Set
 SessionEcho q End = ⊤
-SessionEcho q (Send A S) = Echo (λ _ → ⊤) ⊤
-SessionEcho q (Recv A S) = Echo (λ _ → ⊤) ⊤
-SessionEcho q (Choice S1 S2) = Echo (λ _ → ⊤) ⊤
-SessionEcho q (Select S1 S2) = Echo (λ _ → ⊤) ⊤
+SessionEcho q (Send A S) = Echo {A = ⊤} (λ _ → tt) tt
+SessionEcho q (Recv A S) = Echo {A = ⊤} (λ _ → tt) tt
+SessionEcho q (Choice S1 S2) = Echo {A = ⊤} (λ _ → tt) tt
+SessionEcho q (Select S1 S2) = Echo {A = ⊤} (λ _ → tt) tt
 
 -- Example: Echo over Alice's send protocol
 AliceSendEcho : SessionEcho Alice AliceSendsUnit
-AliceSendEcho = echo-intro (λ _ → tt) tt
-
--- Protocol provenance: echo retains session structure
-ProtocolProvenance : ∀ {p} {S : Session p} {q : Party} → 
-                      SessionEcho q S → Echo (λ _ → ⊤) ⊤
-ProtocolProvenance echo = echo
+AliceSendEcho = echo-intro {A = ⊤} (λ _ → tt) tt
+
+-- Protocol provenance: echo retains session structure. For non-End
+-- sessions SessionEcho q S is already Echo {A = ⊤} (λ _ → tt) tt; for End it
+-- is ⊤ and we synthesize the canonical echo.
+ProtocolProvenance : ∀ {p} {S : Session p} {q : Party} →
+                      SessionEcho q S → Echo {A = ⊤} (λ _ → tt) tt
+ProtocolProvenance {S = End}        _    = echo-intro {A = ⊤} (λ _ → tt) tt
+ProtocolProvenance {S = Send _ _}   echo = echo
+ProtocolProvenance {S = Recv _ _}   echo = echo
+ProtocolProvenance {S = Choice _ _} echo = echo
+ProtocolProvenance {S = Select _ _} echo = echo
 
 -- Dyadic echo: session with echo-indexed provenance
 DyadicEcho : ∀ {p} → Session p → Set
@@ -50,12 +56,19 @@ AliceSendWithProvenance = Alice , AliceSendEcho
 
 -- Bob's receive protocol with provenance
 BobReceiveWithProvenance : DyadicEcho BobReceivesUnit
-BobReceiveWithProvenance = Bob , echo-intro (λ _ → tt) tt
+BobReceiveWithProvenance = Bob , echo-intro {A = ⊤} (λ _ → tt) tt
 
--- Provenance preservation under session concatenation
+-- Provenance preservation under session concatenation. We synthesize
+-- a fresh echo at the concatenated session, since SessionEcho at a
+-- Send/Recv/Choice/Select head is always Echo {A = ⊤} (λ _ → tt) tt and at
+-- End it is ⊤.
 ProvenancePreservation : ∀ {p} {S1 S2 : Session p} →
                           DyadicEcho S1 → DyadicEcho S2 → DyadicEcho (S1 >>= S2)
-ProvenancePreservation (q1 , echo1) (q2 , echo2) = q1 , echo1
+ProvenancePreservation {S1 = End}        _         (q2 , echo2) = q2 , echo2
+ProvenancePreservation {S1 = Send _ _}   (q1 , _)  _            = q1 , echo-intro {A = ⊤} (λ _ → tt) tt
+ProvenancePreservation {S1 = Recv _ _}   (q1 , _)  _            = q1 , echo-intro {A = ⊤} (λ _ → tt) tt
+ProvenancePreservation {S1 = Choice _ _} (q1 , _)  _            = q1 , echo-intro {A = ⊤} (λ _ → tt) tt
+ProvenancePreservation {S1 = Select _ _} (q1 , _)  _            = q1 , echo-intro {A = ⊤} (λ _ → tt) tt
 
 -- Echo-safe dyadic protocols: protocols where echoes preserve safety
 EchoSafe : ∀ {p} → Session p → Set

proofs/agda/Echo.agda

@@ -4,7 +4,7 @@ module Echo where
 
 open import Level using (Level; _⊔_)
 open import Function.Base using (_∘_; id)
-open import Data.Product.Base using (Σ; _,_)
+open import Data.Product.Base using (Σ; _,_; _×_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; cong)
 
 -- Echo_f(y) := Σ (x : A) , (f x ≡ y)
@@ -63,3 +63,35 @@ map-square :
   (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)
+
+-- Composition isomorphism: the echo of g ∘ f at y is canonically
+-- equivalent to a Σ over an intermediate b : B of (Echo f b × g b ≡ y).
+-- This is the accumulation law from docs/echo-types/composition.md §1:
+-- composition does not weaken the intensional core, it accumulates
+-- witness structure. Both round-trips are definitional once the
+-- refl pattern has pinned the intermediate b to f x.
+
+Echo-comp-iso-to :
+  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+  (f : A → B) (g : B → C) {y : C} →
+  Echo (g ∘ f) y → Σ B (λ b → Echo f b × (g b ≡ y))
+Echo-comp-iso-to f g (x , p) = f x , (x , refl) , p
+
+Echo-comp-iso-from :
+  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+  (f : A → B) (g : B → C) {y : C} →
+  Σ B (λ b → Echo f b × (g b ≡ y)) → Echo (g ∘ f) y
+Echo-comp-iso-from f g (b , (x , refl) , p) = x , p
+
+Echo-comp-iso-from-to :
+  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+  (f : A → B) (g : B → C) {y : C} (e : Echo (g ∘ f) y) →
+  Echo-comp-iso-from f g (Echo-comp-iso-to f g e) ≡ e
+Echo-comp-iso-from-to f g (x , p) = refl
+
+Echo-comp-iso-to-from :
+  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+  (f : A → B) (g : B → C) {y : C}
+  (r : Σ B (λ b → Echo f b × (g b ≡ y))) →
+  Echo-comp-iso-to f g (Echo-comp-iso-from f g r) ≡ r
+Echo-comp-iso-to-from f g (b , (x , refl) , p) = refl