Fix DyadicEchoBridge universe error and wire in Dyadic

Three defects kept this file from typechecking:

1. Lines 29-32, 42: the body `Echo (λ _ → ⊤) ⊤` conflated the unit
   *type* (⊤ : Set) with the unit *value* (tt : ⊤). Echo expects a
   function A → B and a value y : B, not a function into Set. Changed
   to `Echo {A = ⊤} (λ _ → tt) tt` — pinning A explicitly because the
   inferred source type is not constrained anywhere else.

2. ProtocolProvenance pattern-matched on a SessionEcho input whose
   type depends on the Session constructor. The End case has type ⊤,
   not Echo, so the single-clause catch-all "ProtocolProvenance echo
   = echo" could not typecheck. Split into five clauses, synthesising
   a canonical Echo in the End case via echo-intro.

3. ProvenancePreservation returned the left echo verbatim, but its
   type was SessionEcho at (S1 >>= S2) rather than at S1. Pattern-
   match on S1 and synthesise a fresh canonical echo at the
   concatenated head; pass the right-hand echo through when S1 = End.

Also wired Dyadic + DyadicEchoBridge into All.agda so they join the
verified suite and cannot silently regress again.

https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK

Author: claude

proofs/agda/All.agda

@@ -22,6 +22,8 @@ open import EchoCategorical
 open import EchoScope
 open import EchoOrdinal
 open import EchoJanusBridge
+open import Dyadic
+open import DyadicEchoBridge
 
 open import Ordinal.Base
 open import Ordinal.Closure

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