agda(EchoEpistemic): fix Agda 2.8.0 inference for knowledge-monotone-{comp,id}

Two surgical changes to keep `--safe --without-K` green under
Agda 2.8.0:

1. `Knows r P y` was defined as `∀ e → P (proj₁ (RoleEcho r y ∋ e))`
   using a where-bound type-ascription operator `_∋_`. Under 2.8.0
   the unifier can no longer see the role/value parameters through
   that indirection, which leaves r and y as unsolved metas in any
   downstream lemma quantifying over `e`. Spelt out as
   `(e : RoleEcho r y) → P (proj₁ e)` — equivalent meaning, no
   ascription helper.

2. `knowledge-monotone-comp` and `knowledge-monotone-id` previously
   used `∀ e → ...` in their signatures, which left e's type as a
   meta. Made the type explicit (`(e : RoleEcho r y) → ...`) and,
   because `obs : Role → Global → Bool` is not injective, supplied
   the implicit `r y P Q R` arguments at every `knowledge-monotone`
   call site inside the equality. The proof body remains `refl` —
   both sides reduce definitionally to
   `qr (proj₁ e) (pq (proj₁ e) (k e))`.

EchoEpistemic.agda now typechecks under `--safe --without-K`. No
postulates introduced. No semantics changed — the lemmas express
the same modal-layer composition rung the previous version
described.

This fix does not touch Ordinal.Brouwer (separately failing under
the in-flight Phase 1.3 recursive-predicate redesign).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/agda/EchoEpistemic.agda

@@ -26,12 +26,12 @@ indist-trans :
 indist-trans = trans
 
 -- Knowledge at visible value y: P holds for every witness compatible with y.
+-- Spelt out as `(e : RoleEcho r y) → ...` rather than `∀ e → ... ∋ e` so
+-- Agda 2.8.0's unifier can see the role and value parameters through
+-- downstream lemmas (knowledge-monotone-comp etc.) without a
+-- type-ascription indirection.
 Knows : Role → (Global → Set) → Bool → Set
-Knows r P y = ∀ e → P (proj₁ (RoleEcho r y ∋ e))
-  where
-    infix 4 _∋_
-    _∋_ : ∀ {ℓ} (A : Set ℓ) → A → A
-    _ ∋ x = x
+Knows r P y = (e : RoleEcho r y) → P (proj₁ e)
 
 knows-from-preimage :
   ∀ {r : Role} {y : Bool} {P : Global → Set} →
@@ -56,14 +56,20 @@ knowledge-monotone pq k e = pq (proj₁ e) (k e)
 -- equation lives inside `--safe --without-K` without function
 -- extensionality. Both sides reduce to `qr (proj₁ e) (pq (proj₁ e)
 -- (k e))` definitionally.
+-- Implicit args to `knowledge-monotone` are annotated explicitly at every
+-- call site. Under Agda 2.8.0 the unifier won't infer the implicit role
+-- `r` from `obs _r x = obs r x` (obs isn't injective), so the
+-- decoration's role+value+predicate parameters must be supplied directly.
 knowledge-monotone-comp :
   ∀ {r : Role} {y : Bool} {P Q R : Global → Set}
   (pq : ∀ g → P g → Q g)
   (qr : ∀ g → Q g → R g)
   (k  : Knows r P y) →
-  ∀ e →
-  knowledge-monotone qr (knowledge-monotone pq k) e
-  ≡ knowledge-monotone (λ g p → qr g (pq g p)) k e
+  (e : RoleEcho r y) →
+    knowledge-monotone {r = r} {y = y} {P = Q} {Q = R} qr
+      (knowledge-monotone {r = r} {y = y} {P = P} {Q = Q} pq k) e
+  ≡ knowledge-monotone {r = r} {y = y} {P = P} {Q = R}
+      (λ g p → qr g (pq g p)) k e
 knowledge-monotone-comp pq qr k e = refl
 
 -- Identity-step corollary: monotonicity along the identity predicate
@@ -72,8 +78,9 @@ knowledge-monotone-comp pq qr k e = refl
 knowledge-monotone-id :
   ∀ {r : Role} {y : Bool} {P : Global → Set}
   (k : Knows r P y) →
-  ∀ e →
-  knowledge-monotone (λ _ p → p) k e ≡ k e
+  (e : RoleEcho r y) →
+    knowledge-monotone {r = r} {y = y} {P = P} {Q = P} (λ _ p → p) k e
+  ≡ k e
 knowledge-monotone-id k e = refl
 
 ServerIsTrue : Global → Set