agda(EchoChoreo): per-decoration composition rung — closes 5-decoration sweep (#24)

## Summary

- Adds the per-decoration composition rung to \`EchoChoreo.agda\`:
choreographic-reachability order \`_⊑c_\` (3 constructors),
transitivity, propositionality, \`applyChoreo\`, \`applyChoreo-comp\`,
join \`_⊔c_\` with axioms, factoring-free \`applyChoreo-compose\`, and
\`applyChoreo-via-join\` restatement.
- Closes the five-decoration sweep started by
\`EchoGraded.degrade-compose\` and continued through \`EchoLinear\`,
\`EchoIndexed\`, \`EchoEpistemic\`. The role/choreo case now sits in the
same shape as the rest.
- Pinned in \`Smoke.agda\` (10 new headlines).
- \`docs/echo-types/composition.md\` §6 updated to mark the rung closed.

## Why this design

The Choreo decoration is the role choice (Client/Server). The canonical
lift is \`client-to-server\` via the swap-based map-square. Restricting
the order to one-way \`Client ⊑c Server\` (not the reverse) keeps the
rung non-degenerate — the reverse swap exists but including it would
make \`_⊑c_\` an equivalence and collapse the join.

## Compile-verification

\`\`\`
agda -i proofs/agda proofs/agda/All.agda
agda -i proofs/agda proofs/agda/Smoke.agda
\`\`\`

Both exit 0 under \`--safe --without-K\`. No postulates introduced.

## Test plan

- [ ] \`agda -i proofs/agda proofs/agda/All.agda\` exits 0
- [ ] \`agda -i proofs/agda proofs/agda/Smoke.agda\` exits 0
- [ ] \`grep -n postulate proofs/agda/EchoChoreo.agda\` returns nothing
- [ ] All 10 new \`EchoChoreo\` headlines pin in \`Smoke.agda\`

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Author: hyperpolymath

docs/echo-types/composition.md

@@ -276,13 +276,20 @@ Ranked by unblock-value. (1) and (2) landed; (3) onwards is open.
    `echo-approx-relax`, and `echo-approx-compose` (additive under
    non-expansive outer leg).
 6. **Decoration commuting.** Per-decoration lemmas in the existing
-   `EchoGraded`, `EchoLinear`, `EchoIndexed` modules. *Grade case
-   landed*: `EchoGraded.degrade-compose` (per-decoration composition
-   law) and `degrade-via-join` (its join-structured restatement),
-   resting on `≤g-prop` and `degrade-comp`. *Linear case landed*:
-   `EchoLinear.degradeMode-comp` along the mode order with
-   `degradeMode-id-{linear, affine}` corollaries. Indexed / role /
-   modal still open.
+   `EchoGraded`, `EchoLinear`, `EchoIndexed`, `EchoChoreo`,
+   `EchoEpistemic` modules. *Grade case landed*: `EchoGraded.degrade-compose`
+   (per-decoration composition law) and `degrade-via-join` (its
+   join-structured restatement), resting on `≤g-prop` and `degrade-comp`.
+   *Linear case landed*: `EchoLinear.degradeMode-{comp,compose,via-join}`
+   along the two-mode order. *Indexed case landed*:
+   `EchoIndexed.map-role-indexed-comp`. *Modal case landed*:
+   `EchoEpistemic.knowledge-monotone-comp` (with `knowledge-monotone-id`
+   identity-step corollary). *Role/choreo case landed*:
+   `EchoChoreo.applyChoreo-{comp,compose,via-join}` along the
+   choreographic-reachability order `_⊑c_` (`Client ⊑c Server`),
+   resting on `⊑c-prop` and the canonical `_⊔c_` join. The
+   five-decoration sweep is now closed at the per-decoration
+   composition rung.
 
 None of these depend on the blocked Buchholz-WF / shared-binder
 work. All are Sonnet-class proofs; (5) is Opus 4.7 design and

proofs/agda/EchoChoreo.agda

@@ -85,3 +85,137 @@ client-preimage-class :
   proj₁ (proj₁ e) ≡ true × (proj₂ (proj₁ e) ≡ true ⊎ proj₂ (proj₁ e) ≡ false)
 client-preimage-class ((true , true) , refl) = refl , inj₁ refl
 client-preimage-class ((true , false) , refl) = refl , inj₂ refl
+
+----------------------------------------------------------------------
+-- Per-decoration composition rung.
+--
+-- The Choreo decoration is the choice of role: Client or Server.
+-- The natural "decoration order" is choreographic reachability —
+-- whether a one-way map-square lift takes a `RoleEcho r1 y` to a
+-- `RoleEcho r2 y`. Restricting to the canonical lift `client-to-server`
+-- (and the reflexive self-loops) gives a 2-element chain
+-- `Client ⊑c Server` with three constructors. The reverse step
+-- `server-to-client` exists too (swap is involutive), but is not
+-- part of the canonical degradation — including it would make the
+-- order an equivalence and collapse the rung.
+--
+-- This is the role/modal analogue of `EchoGraded.degrade-compose`,
+-- `EchoLinear.degradeMode-compose`, `EchoIndexed.map-role-indexed-comp`
+-- and `EchoEpistemic.knowledge-monotone-comp`. The standard recipe
+-- — order, transitivity, propositionality, apply, apply-comp,
+-- join, factoring-free compose, via-join restatement — runs
+-- through with all proofs definitional once the propositional
+-- order is in hand.
+--
+-- Headlines (pinned in Smoke.agda):
+--
+--   * _⊑c_                 -- choreographic reachability order
+--   * ⊑c-trans             -- transitivity
+--   * ⊑c-prop              -- the order is propositional
+--   * applyChoreo          -- transport an echo along the order
+--   * applyChoreo-comp     -- decomposition: trans equals nesting
+--   * _⊔c_                 -- join (Server is top)
+--   * ⊑c-⊔c-{left,right,univ}
+--   * applyChoreo-compose  -- factoring-free composition law
+--   * applyChoreo-via-join -- restated via the join
+
+data _⊑c_ : Role → Role → Set where
+  c⊑c : Client ⊑c Client
+  c⊑s : Client ⊑c Server
+  s⊑s : Server ⊑c Server
+
+⊑c-trans : ∀ {r1 r2 r3 : Role} → r1 ⊑c r2 → r2 ⊑c r3 → r1 ⊑c r3
+⊑c-trans c⊑c c⊑c = c⊑c
+⊑c-trans c⊑c c⊑s = c⊑s
+⊑c-trans c⊑s s⊑s = c⊑s
+⊑c-trans s⊑s s⊑s = s⊑s
+
+-- The order is propositional: any two proofs of `r1 ⊑c r2` agree.
+-- A discharge clause per constructor is enough; there are no
+-- shared-binder cases on this 3-constructor data type.
+⊑c-prop : ∀ {r1 r2 : Role} (p1 p2 : r1 ⊑c r2) → p1 ≡ p2
+⊑c-prop c⊑c c⊑c = refl
+⊑c-prop c⊑s c⊑s = refl
+⊑c-prop s⊑s s⊑s = refl
+
+-- Transport an echo along the order. The reflexive cases are
+-- definitional identities; the strict step `c⊑s` invokes the
+-- existing `client-to-server` map-square lift.
+applyChoreo :
+  ∀ {r1 r2 : Role} → r1 ⊑c r2 →
+  ∀ {y : Bool} → RoleEcho r1 y → RoleEcho r2 y
+applyChoreo c⊑c e = e
+applyChoreo c⊑s e = client-to-server e
+applyChoreo s⊑s e = e
+
+-- Decomposition: composing two ⊑c-steps via `⊑c-trans` and then
+-- transporting agrees with transporting twice. Closes `refl` on
+-- every reachable constructor pair (4 cases out of the 9 syntactic
+-- pairings).
+applyChoreo-comp :
+  ∀ {r1 r2 r3 : Role}
+  (p12 : r1 ⊑c r2) (p23 : r2 ⊑c r3)
+  {y : Bool} (e : RoleEcho r1 y) →
+  applyChoreo (⊑c-trans p12 p23) e ≡ applyChoreo p23 (applyChoreo p12 e)
+applyChoreo-comp c⊑c c⊑c e = refl
+applyChoreo-comp c⊑c c⊑s e = refl
+applyChoreo-comp c⊑s s⊑s e = refl
+applyChoreo-comp s⊑s s⊑s e = refl
+
+-- Join structure: Server is the top role. The join is the role
+-- with strictly more "view" — `Server` whenever either argument
+-- is `Server`, otherwise `Client`.
+_⊔c_ : Role → Role → Role
+Client ⊔c Client = Client
+Client ⊔c Server = Server
+Server ⊔c Client = Server
+Server ⊔c Server = Server
+
+⊑c-⊔c-left : ∀ (r1 r2 : Role) → r1 ⊑c (r1 ⊔c r2)
+⊑c-⊔c-left Client Client = c⊑c
+⊑c-⊔c-left Client Server = c⊑s
+⊑c-⊔c-left Server Client = s⊑s
+⊑c-⊔c-left Server Server = s⊑s
+
+⊑c-⊔c-right : ∀ (r1 r2 : Role) → r2 ⊑c (r1 ⊔c r2)
+⊑c-⊔c-right Client Client = c⊑c
+⊑c-⊔c-right Client Server = s⊑s
+⊑c-⊔c-right Server Client = c⊑s
+⊑c-⊔c-right Server Server = s⊑s
+
+⊑c-⊔c-univ : ∀ {r1 r2 r3 : Role} → r1 ⊑c r3 → r2 ⊑c r3 → (r1 ⊔c r2) ⊑c r3
+⊑c-⊔c-univ {Client} {Client} c⊑c c⊑c = c⊑c
+⊑c-⊔c-univ {Client} {Client} c⊑s c⊑s = c⊑s
+⊑c-⊔c-univ {Client} {Server} c⊑s s⊑s = s⊑s
+⊑c-⊔c-univ {Server} {Client} s⊑s c⊑s = s⊑s
+⊑c-⊔c-univ {Server} {Server} s⊑s s⊑s = s⊑s
+
+-- Factoring-free composition: any direct r1 ⊑c r3 lift agrees
+-- with any factoring r1 ⊑c r2 ⊑c r3, by `applyChoreo-comp` plus
+-- `⊑c-prop` on `p13` vs `⊑c-trans p12 p23`. The role/modal
+-- analogue of `EchoGraded.degrade-compose`.
+applyChoreo-compose :
+  ∀ {r1 r2 r3 : Role}
+  (p12 : r1 ⊑c r2) (p23 : r2 ⊑c r3) (p13 : r1 ⊑c r3)
+  {y : Bool} (e : RoleEcho r1 y) →
+  applyChoreo p23 (applyChoreo p12 e) ≡ applyChoreo p13 e
+applyChoreo-compose p12 p23 p13 e
+  rewrite ⊑c-prop p13 (⊑c-trans p12 p23)
+        = sym (applyChoreo-comp p12 p23 e)
+  where open import Relation.Binary.PropositionalEquality using (sym)
+
+-- Via-join restatement: for any two paths `p1, p2 : r1 ⊑c r3`,
+-- transporting along `p1` agrees with going through the join
+-- `r1 ⊔c r2` and then up to r3 via the universal property.
+-- (When r2 = r1 the join is r1 and the LHS = RHS definitionally.)
+applyChoreo-via-join :
+  ∀ {r1 r3 : Role} (r2 : Role)
+  (p1 : r1 ⊑c r3) (p2 : r2 ⊑c r3)
+  {y : Bool} (e : RoleEcho r1 y) →
+  applyChoreo p1 e
+  ≡ applyChoreo (⊑c-⊔c-univ p1 p2) (applyChoreo (⊑c-⊔c-left r1 r2) e)
+applyChoreo-via-join {Client} {Client} Client c⊑c c⊑c e = refl
+applyChoreo-via-join {Client} {Server} Client c⊑s c⊑s e = refl
+applyChoreo-via-join {Client} {Server} Server c⊑s s⊑s e = refl
+applyChoreo-via-join {Server} {Server} Client s⊑s c⊑s e = refl
+applyChoreo-via-join {Server} {Server} Server s⊑s s⊑s e = refl

proofs/agda/Smoke.agda

@@ -89,6 +89,17 @@ open import EchoChoreo using
   ; client-to-server
   ; client-stability
   ; client-preimage-class
+  ; _⊑c_
+  ; ⊑c-trans
+  ; ⊑c-prop
+  ; applyChoreo
+  ; applyChoreo-comp
+  ; _⊔c_
+  ; ⊑c-⊔c-left
+  ; ⊑c-⊔c-right
+  ; ⊑c-⊔c-univ
+  ; applyChoreo-compose
+  ; applyChoreo-via-join
   )
 
 open import EchoEpistemic using