agda(truncation): rename level variables to avoid name shadow

The `private variable a b : Level` block at the top of EchoTruncation.agda
shadowed the constructors `EchoTropical.Candidate.a` and
`EchoTropical.Candidate.b` once `open import EchoTropical using (...; a; b; ...)`
was in scope inside `module TropicalExample`. Agda 2.8.0 + stdlib v2.0
flagged the ambiguity:

  EchoTruncation.agda:144.25-26: error: [AmbiguousName]
  Ambiguous name a. ...

Renaming to `ℓa ℓb : Level` makes the level variables non-conflicting
with any imported example's term-level names while keeping the
universe-polymorphism intact.

Done-test now passes:
  agda --safe -i proofs/agda proofs/agda/EchoTruncation.agda  # exit 0

(Verified locally on Ubuntu WSL with the prebuilt Agda 2.8.0 Linux
binary + agda-stdlib v2.0.)

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

Author: hyperpolymath

proofs/agda/EchoTruncation.agda

@@ -26,9 +26,9 @@ open import Relation.Nullary using (¬_)
 
 private
   variable
-    a b : Level
-    A : Set a
-    B : Set b
+    ℓa ℓb : Level
+    A : Set ℓa
+    B : Set ℓb
 
 -- A type is propositional ("a mere proposition") when any two
 -- inhabitants are equal. Standard HoTT terminology, kept universe-