fix(EchoAccess): correct ≤a-⊔a-univ constructor RHS where c1 ⊔a c2 = c2

The previous commit's `≤a-⊔a-univ` clauses contained 10 wrong-RHS bugs
in the rows where the join reduces to the second summand (`c1 < c2`
on the chain). When `c1 ⊔a c2 = c2`, the required witness has type
`c2 ≤a c` (i.e. it must equal `p2`), but the buggy clauses returned
`p1 : c1 ≤a c` — a different inequality constructor.

The parent verifier caught the first failure:

    EchoAccess.agda:400.58-72: error: [UnequalTerms]
    decidable != enum of type Access
    when checking that the expression decidable≤enum has type
    (decidable ⊔a enum) ≤a enum

`_⊔a_` was reducing correctly; the bug was on the right-hand side
of the universal-property clauses.

Audit by `(c1, c2)` pair with `c1 < c2`:
  * decidable < enum/feasible/infeasible  (3 c values × 3 pairs)
  * enum      < feasible/infeasible       (2 c values × 2 pairs)
  * feasible  < infeasible                 (1 c value × 1 pair)

That's exactly 10 clauses, each now corrected to return the
appropriate `c2 ≤a c` constructor (equivalent to returning `p2`
directly; the explicit-constructor form is kept for consistency with
the rest of the file).

`≤a-⊔a-{left, right}` and `degrade-access-{comp, compose, via-join}`
were re-audited under the same lens; no further bugs found
(`≤a-⊔a-left` returns a `c1 ≤a (c1 ⊔a c2)` witness which is always
the unique constructor from `c1` to the larger of the two,
`≤a-⊔a-right` likewise returns the `c2`-rooted witness, both already
correct).

BUILD STILL UNVERIFIED LOCALLY — sandbox continues to block `agda`
invocations on positional file arguments. Parent verifier please
re-run.

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

Author: hyperpolymath

proofs/agda/EchoAccess.agda

@@ -397,28 +397,28 @@ infeasible ⊔a _          = infeasible
 ≤a-⊔a-univ decidable≤decidable   decidable≤decidable   = decidable≤decidable
 ≤a-⊔a-univ decidable≤enum        free≤enum             = decidable≤enum
 ≤a-⊔a-univ decidable≤enum        decidable≤enum        = decidable≤enum
-≤a-⊔a-univ decidable≤enum        enum≤enum             = decidable≤enum
+≤a-⊔a-univ decidable≤enum        enum≤enum             = enum≤enum
 ≤a-⊔a-univ decidable≤feasible    free≤feasible         = decidable≤feasible
 ≤a-⊔a-univ decidable≤feasible    decidable≤feasible    = decidable≤feasible
-≤a-⊔a-univ decidable≤feasible    enum≤feasible         = decidable≤feasible
-≤a-⊔a-univ decidable≤feasible    feasible≤feasible     = decidable≤feasible
+≤a-⊔a-univ decidable≤feasible    enum≤feasible         = enum≤feasible
+≤a-⊔a-univ decidable≤feasible    feasible≤feasible     = feasible≤feasible
 ≤a-⊔a-univ decidable≤infeasible  free≤infeasible       = decidable≤infeasible
 ≤a-⊔a-univ decidable≤infeasible  decidable≤infeasible  = decidable≤infeasible
-≤a-⊔a-univ decidable≤infeasible  enum≤infeasible       = decidable≤infeasible
-≤a-⊔a-univ decidable≤infeasible  feasible≤infeasible   = decidable≤infeasible
-≤a-⊔a-univ decidable≤infeasible  infeasible≤infeasible = decidable≤infeasible
+≤a-⊔a-univ decidable≤infeasible  enum≤infeasible       = enum≤infeasible
+≤a-⊔a-univ decidable≤infeasible  feasible≤infeasible   = feasible≤infeasible
+≤a-⊔a-univ decidable≤infeasible  infeasible≤infeasible = infeasible≤infeasible
 ≤a-⊔a-univ enum≤enum             free≤enum             = enum≤enum
 ≤a-⊔a-univ enum≤enum             decidable≤enum        = enum≤enum
 ≤a-⊔a-univ enum≤enum             enum≤enum             = enum≤enum
 ≤a-⊔a-univ enum≤feasible         free≤feasible         = enum≤feasible
 ≤a-⊔a-univ enum≤feasible         decidable≤feasible    = enum≤feasible
 ≤a-⊔a-univ enum≤feasible         enum≤feasible         = enum≤feasible
-≤a-⊔a-univ enum≤feasible         feasible≤feasible     = enum≤feasible
+≤a-⊔a-univ enum≤feasible         feasible≤feasible     = feasible≤feasible
 ≤a-⊔a-univ enum≤infeasible       free≤infeasible       = enum≤infeasible
 ≤a-⊔a-univ enum≤infeasible       decidable≤infeasible  = enum≤infeasible
 ≤a-⊔a-univ enum≤infeasible       enum≤infeasible       = enum≤infeasible
-≤a-⊔a-univ enum≤infeasible       feasible≤infeasible   = enum≤infeasible
-≤a-⊔a-univ enum≤infeasible       infeasible≤infeasible = enum≤infeasible
+≤a-⊔a-univ enum≤infeasible       feasible≤infeasible   = feasible≤infeasible
+≤a-⊔a-univ enum≤infeasible       infeasible≤infeasible = infeasible≤infeasible
 ≤a-⊔a-univ feasible≤feasible     free≤feasible         = feasible≤feasible
 ≤a-⊔a-univ feasible≤feasible     decidable≤feasible    = feasible≤feasible
 ≤a-⊔a-univ feasible≤feasible     enum≤feasible         = feasible≤feasible
@@ -427,7 +427,7 @@ infeasible ⊔a _          = infeasible
 ≤a-⊔a-univ feasible≤infeasible   decidable≤infeasible  = feasible≤infeasible
 ≤a-⊔a-univ feasible≤infeasible   enum≤infeasible       = feasible≤infeasible
 ≤a-⊔a-univ feasible≤infeasible   feasible≤infeasible   = feasible≤infeasible
-≤a-⊔a-univ feasible≤infeasible   infeasible≤infeasible = feasible≤infeasible
+≤a-⊔a-univ feasible≤infeasible   infeasible≤infeasible = infeasible≤infeasible
 ≤a-⊔a-univ infeasible≤infeasible free≤infeasible       = infeasible≤infeasible
 ≤a-⊔a-univ infeasible≤infeasible decidable≤infeasible  = infeasible≤infeasible
 ≤a-⊔a-univ infeasible≤infeasible enum≤infeasible       = infeasible≤infeasible