3535-- 5. `EchoAccess` — Σ-shape carrier indexed by `Access`
3636-- 6. `access-of`,
3737-- `degrade-access` — projection + ≤a-indexed degrade primitive
38+ -- 7. `_⊔a_`,
39+ -- `≤a-⊔a-{left,right,univ}` — categorical join structure
40+ -- 8. `degrade-access-comp`,
41+ -- `degrade-access-compose`,
42+ -- `degrade-access-via-join` — per-decoration composition; the
43+ -- "factoring-free" closer chain of
44+ -- `composition.md` §6.
3845--
39- -- Deferred to follow-up (the design doc §5 obligations 5–8):
46+ -- Sections 7–8 close the design doc's §5 obligations 5–8 and complete
47+ -- the same recipe `EchoGraded` and `EchoLinear` close at the
48+ -- per-decoration composition rung.
49+ --
50+ -- Deferred to follow-up (the design doc's §6 mode-B mitigation):
4051--
41- -- * `degrade-access-comp`, `degrade-access-compose`,
42- -- `degrade-access-via-join` — per-decoration composition; the
43- -- "factoring-free" closer chain of `composition.md` §6.
44- -- * `_⊔a_` join + `≤a-⊔a-{left,right,univ}` — categorical join
45- -- structure.
4652-- * Honest carrier for `enum` (bridge to `EchoFiberCount.FiberSize-fin`)
47- -- so `feasible` / `infeasible` are not Potemkin labels — the
48- -- falsifier mode B of the design's §6. The current carriers are
49- -- deliberately the minimal placeholders that let the order layer
50- -- ship green.
53+ -- so `feasible` / `infeasible` are not Potemkin labels. This is
54+ -- **not** a code-mechanical extension — it requires a design
55+ -- decision: an honest `enum`-grade carrier must package an
56+ -- enumerator `Fin n → A` and a decider on `B`, neither of which
57+ -- can be supplied without breaking the parametricity over `A`
58+ -- that `Echo f y` enjoys at the `free` grade. The two cleanest
59+ -- resolutions are (a) parameterise the whole `CEcho` family on
60+ -- `Decidable B` + an enumeration witness (forces every caller to
61+ -- supply them, even at the `free` grade where they do nothing),
62+ -- or (b) bury both in an existential inside the `enum` /
63+ -- `feasible` / `infeasible` cases (loses the ability to extract
64+ -- the enumerator from outside). Both are real architectural
65+ -- choices; see the design doc's §6 falsifier mode B. The current
66+ -- carriers for `enum` / `feasible` / `infeasible` remain the
67+ -- minimal `Lift ⊤` placeholder — the grade still names the loss
68+ -- (same design as `EchoGraded.forget = ⊤`), the composition layer
69+ -- above this module is grade-indexed not carrier-indexed, and
70+ -- therefore is unaffected by the eventual carrier choice.
5171
5272module EchoAccess where
5373
5474open import Level using (Level; _⊔_)
5575open import Data.Unit.Base using (⊤; tt)
5676open import Data.Product.Base using (Σ; _,_)
5777open import Relation.Nullary.Decidable.Core using (yes)
58- open import Relation.Binary.PropositionalEquality using (_≡_; refl)
78+ open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym )
5979
6080open import Echo using (Echo)
6181open import EchoDecidable using (EchoDec)
@@ -237,10 +257,11 @@ access-of (c , _) = c
237257-- content moves; from `enum` onward the carrier is already `⊤`-lifted
238258-- so every transition is `lift tt`.
239259--
240- -- Per-decoration composition (`degrade-access-comp` + `compose` +
241- -- `via-join`) is deferred to the follow-up PR per the body of this
242- -- module. The order layer (`≤a-trans`, `≤a-prop`) is the
243- -- mathematical prerequisite for that follow-up, and lands here.
260+ -- The per-decoration composition trio
261+ -- (`degrade-access-comp` / `compose` / `via-join`) and the join
262+ -- structure (`_⊔a_` + universal property) follow this section — the
263+ -- order layer (`≤a-trans`, `≤a-prop`) is their mathematical
264+ -- prerequisite.
244265
245266degrade-access :
246267 ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B}
@@ -260,3 +281,233 @@ degrade-access enum≤infeasible _ = lift tt
260281degrade-access feasible≤feasible e = e
261282degrade-access feasible≤infeasible _ = lift tt
262283degrade-access infeasible≤infeasible e = e
284+
285+ ----------------------------------------------------------------------
286+ -- 7. The access join
287+ ----------------------------------------------------------------------
288+
289+ -- Componentwise max along the chain
290+ -- `free ≤ decidable ≤ enum ≤ feasible ≤ infeasible`. `free` is bottom
291+ -- (`free ⊔a c = c`); `infeasible` is top (`infeasible ⊔a _ = infeasible`).
292+ -- Same shape as `EchoGraded._⊔g_` and `EchoLinear._⊔m_`, only widened
293+ -- to five grades. Enumeration is forced once the bottom and top
294+ -- absorbing cases are fixed.
295+
296+ _⊔a_ : Access → Access → Access
297+ free ⊔a c2 = c2
298+ decidable ⊔a free = decidable
299+ decidable ⊔a decidable = decidable
300+ decidable ⊔a enum = enum
301+ decidable ⊔a feasible = feasible
302+ decidable ⊔a infeasible = infeasible
303+ enum ⊔a free = enum
304+ enum ⊔a decidable = enum
305+ enum ⊔a enum = enum
306+ enum ⊔a feasible = feasible
307+ enum ⊔a infeasible = infeasible
308+ feasible ⊔a free = feasible
309+ feasible ⊔a decidable = feasible
310+ feasible ⊔a enum = feasible
311+ feasible ⊔a feasible = feasible
312+ feasible ⊔a infeasible = infeasible
313+ infeasible ⊔a _ = infeasible
314+
315+ -- Join is an upper bound on its left summand. The proof enumerates
316+ -- the 25 reachable `(c1, c2)` pairs; each picks out the unique
317+ -- inhabitant of `_≤a_` from `c1` to `c1 ⊔a c2`. Mirrors
318+ -- `EchoGraded.≤g-⊔g-left` and `EchoLinear.≤m-⊔m-left`.
319+
320+ ≤a-⊔a-left : ∀ c1 c2 → c1 ≤a (c1 ⊔a c2)
321+ ≤a-⊔a-left free free = free≤free
322+ ≤a-⊔a-left free decidable = free≤decidable
323+ ≤a-⊔a-left free enum = free≤enum
324+ ≤a-⊔a-left free feasible = free≤feasible
325+ ≤a-⊔a-left free infeasible = free≤infeasible
326+ ≤a-⊔a-left decidable free = decidable≤decidable
327+ ≤a-⊔a-left decidable decidable = decidable≤decidable
328+ ≤a-⊔a-left decidable enum = decidable≤enum
329+ ≤a-⊔a-left decidable feasible = decidable≤feasible
330+ ≤a-⊔a-left decidable infeasible = decidable≤infeasible
331+ ≤a-⊔a-left enum free = enum≤enum
332+ ≤a-⊔a-left enum decidable = enum≤enum
333+ ≤a-⊔a-left enum enum = enum≤enum
334+ ≤a-⊔a-left enum feasible = enum≤feasible
335+ ≤a-⊔a-left enum infeasible = enum≤infeasible
336+ ≤a-⊔a-left feasible free = feasible≤feasible
337+ ≤a-⊔a-left feasible decidable = feasible≤feasible
338+ ≤a-⊔a-left feasible enum = feasible≤feasible
339+ ≤a-⊔a-left feasible feasible = feasible≤feasible
340+ ≤a-⊔a-left feasible infeasible = feasible≤infeasible
341+ ≤a-⊔a-left infeasible free = infeasible≤infeasible
342+ ≤a-⊔a-left infeasible decidable = infeasible≤infeasible
343+ ≤a-⊔a-left infeasible enum = infeasible≤infeasible
344+ ≤a-⊔a-left infeasible feasible = infeasible≤infeasible
345+ ≤a-⊔a-left infeasible infeasible = infeasible≤infeasible
346+
347+ -- Join is an upper bound on its right summand. Same shape.
348+
349+ ≤a-⊔a-right : ∀ c1 c2 → c2 ≤a (c1 ⊔a c2)
350+ ≤a-⊔a-right free free = free≤free
351+ ≤a-⊔a-right free decidable = decidable≤decidable
352+ ≤a-⊔a-right free enum = enum≤enum
353+ ≤a-⊔a-right free feasible = feasible≤feasible
354+ ≤a-⊔a-right free infeasible = infeasible≤infeasible
355+ ≤a-⊔a-right decidable free = free≤decidable
356+ ≤a-⊔a-right decidable decidable = decidable≤decidable
357+ ≤a-⊔a-right decidable enum = enum≤enum
358+ ≤a-⊔a-right decidable feasible = feasible≤feasible
359+ ≤a-⊔a-right decidable infeasible = infeasible≤infeasible
360+ ≤a-⊔a-right enum free = free≤enum
361+ ≤a-⊔a-right enum decidable = decidable≤enum
362+ ≤a-⊔a-right enum enum = enum≤enum
363+ ≤a-⊔a-right enum feasible = feasible≤feasible
364+ ≤a-⊔a-right enum infeasible = infeasible≤infeasible
365+ ≤a-⊔a-right feasible free = free≤feasible
366+ ≤a-⊔a-right feasible decidable = decidable≤feasible
367+ ≤a-⊔a-right feasible enum = enum≤feasible
368+ ≤a-⊔a-right feasible feasible = feasible≤feasible
369+ ≤a-⊔a-right feasible infeasible = infeasible≤infeasible
370+ ≤a-⊔a-right infeasible free = free≤infeasible
371+ ≤a-⊔a-right infeasible decidable = decidable≤infeasible
372+ ≤a-⊔a-right infeasible enum = enum≤infeasible
373+ ≤a-⊔a-right infeasible feasible = feasible≤infeasible
374+ ≤a-⊔a-right infeasible infeasible = infeasible≤infeasible
375+
376+ -- Universal property of join: anything dominated by both `c1` and
377+ -- `c2` is dominated by their join. Together with the two upper-bound
378+ -- lemmas above this exhibits `_⊔a_` as the categorical join in
379+ -- `_≤a_`. Same recipe as `EchoGraded.≤g-⊔g-univ` and
380+ -- `EchoLinear.≤m-⊔m-univ`.
381+ --
382+ -- The pattern-match strategy: case-split on the first inequality `p1`
383+ -- so the join `c1 ⊔a c2` reduces enough for Agda to see the
384+ -- constructor needed in the result. Where `c1 = free`, the join is
385+ -- `c2` and the result is just `p2`. For other rows, case-split on
386+ -- `p2` and read off the unique inhabitant of `_≤a_` from
387+ -- `(c1 ⊔a c2)` to the common upper bound.
388+
389+ ≤a-⊔a-univ :
390+ ∀ {c1 c2 c} → c1 ≤a c → c2 ≤a c → (c1 ⊔a c2) ≤a c
391+ ≤a-⊔a-univ free≤free p2 = p2
392+ ≤a-⊔a-univ free≤decidable p2 = p2
393+ ≤a-⊔a-univ free≤enum p2 = p2
394+ ≤a-⊔a-univ free≤feasible p2 = p2
395+ ≤a-⊔a-univ free≤infeasible p2 = p2
396+ ≤a-⊔a-univ decidable≤decidable free≤decidable = decidable≤decidable
397+ ≤a-⊔a-univ decidable≤decidable decidable≤decidable = decidable≤decidable
398+ ≤a-⊔a-univ decidable≤enum free≤enum = decidable≤enum
399+ ≤a-⊔a-univ decidable≤enum decidable≤enum = decidable≤enum
400+ ≤a-⊔a-univ decidable≤enum enum≤enum = decidable≤enum
401+ ≤a-⊔a-univ decidable≤feasible free≤feasible = decidable≤feasible
402+ ≤a-⊔a-univ decidable≤feasible decidable≤feasible = decidable≤feasible
403+ ≤a-⊔a-univ decidable≤feasible enum≤feasible = decidable≤feasible
404+ ≤a-⊔a-univ decidable≤feasible feasible≤feasible = decidable≤feasible
405+ ≤a-⊔a-univ decidable≤infeasible free≤infeasible = decidable≤infeasible
406+ ≤a-⊔a-univ decidable≤infeasible decidable≤infeasible = decidable≤infeasible
407+ ≤a-⊔a-univ decidable≤infeasible enum≤infeasible = decidable≤infeasible
408+ ≤a-⊔a-univ decidable≤infeasible feasible≤infeasible = decidable≤infeasible
409+ ≤a-⊔a-univ decidable≤infeasible infeasible≤infeasible = decidable≤infeasible
410+ ≤a-⊔a-univ enum≤enum free≤enum = enum≤enum
411+ ≤a-⊔a-univ enum≤enum decidable≤enum = enum≤enum
412+ ≤a-⊔a-univ enum≤enum enum≤enum = enum≤enum
413+ ≤a-⊔a-univ enum≤feasible free≤feasible = enum≤feasible
414+ ≤a-⊔a-univ enum≤feasible decidable≤feasible = enum≤feasible
415+ ≤a-⊔a-univ enum≤feasible enum≤feasible = enum≤feasible
416+ ≤a-⊔a-univ enum≤feasible feasible≤feasible = enum≤feasible
417+ ≤a-⊔a-univ enum≤infeasible free≤infeasible = enum≤infeasible
418+ ≤a-⊔a-univ enum≤infeasible decidable≤infeasible = enum≤infeasible
419+ ≤a-⊔a-univ enum≤infeasible enum≤infeasible = enum≤infeasible
420+ ≤a-⊔a-univ enum≤infeasible feasible≤infeasible = enum≤infeasible
421+ ≤a-⊔a-univ enum≤infeasible infeasible≤infeasible = enum≤infeasible
422+ ≤a-⊔a-univ feasible≤feasible free≤feasible = feasible≤feasible
423+ ≤a-⊔a-univ feasible≤feasible decidable≤feasible = feasible≤feasible
424+ ≤a-⊔a-univ feasible≤feasible enum≤feasible = feasible≤feasible
425+ ≤a-⊔a-univ feasible≤feasible feasible≤feasible = feasible≤feasible
426+ ≤a-⊔a-univ feasible≤infeasible free≤infeasible = feasible≤infeasible
427+ ≤a-⊔a-univ feasible≤infeasible decidable≤infeasible = feasible≤infeasible
428+ ≤a-⊔a-univ feasible≤infeasible enum≤infeasible = feasible≤infeasible
429+ ≤a-⊔a-univ feasible≤infeasible feasible≤infeasible = feasible≤infeasible
430+ ≤a-⊔a-univ feasible≤infeasible infeasible≤infeasible = feasible≤infeasible
431+ ≤a-⊔a-univ infeasible≤infeasible free≤infeasible = infeasible≤infeasible
432+ ≤a-⊔a-univ infeasible≤infeasible decidable≤infeasible = infeasible≤infeasible
433+ ≤a-⊔a-univ infeasible≤infeasible enum≤infeasible = infeasible≤infeasible
434+ ≤a-⊔a-univ infeasible≤infeasible feasible≤infeasible = infeasible≤infeasible
435+ ≤a-⊔a-univ infeasible≤infeasible infeasible≤infeasible = infeasible≤infeasible
436+
437+ ----------------------------------------------------------------------
438+ -- 8. Per-decoration composition
439+ ----------------------------------------------------------------------
440+
441+ -- The keystone lemma: two successive degrades along a factoring
442+ -- `c1 ≤a c2 ≤a c3` agree with a single degrade along the composed
443+ -- ordering proof. Mirrors `EchoGraded.degrade-comp` and
444+ -- `EchoLinear.degradeMode-comp`. Closes `refl` on every reachable
445+ -- `(p12, p23)` constructor pair: the carriers reduce definitionally
446+ -- in lock-step with `≤a-trans`, so on both sides Agda lands on the
447+ -- same canonical form.
448+
449+ degrade-access-comp :
450+ ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B}
451+ {c1 c2 c3 : Access}
452+ (p12 : c1 ≤a c2)
453+ (p23 : c2 ≤a c3)
454+ (e : CEcho c1 f y) →
455+ degrade-access p23 (degrade-access p12 e)
456+ ≡ degrade-access (≤a-trans p12 p23) e
457+ degrade-access-comp free≤free p23 e = refl
458+ degrade-access-comp free≤decidable decidable≤decidable e = refl
459+ degrade-access-comp free≤decidable decidable≤enum e = refl
460+ degrade-access-comp free≤decidable decidable≤feasible e = refl
461+ degrade-access-comp free≤decidable decidable≤infeasible e = refl
462+ degrade-access-comp free≤enum enum≤enum e = refl
463+ degrade-access-comp free≤enum enum≤feasible e = refl
464+ degrade-access-comp free≤enum enum≤infeasible e = refl
465+ degrade-access-comp free≤feasible feasible≤feasible e = refl
466+ degrade-access-comp free≤feasible feasible≤infeasible e = refl
467+ degrade-access-comp free≤infeasible infeasible≤infeasible e = refl
468+ degrade-access-comp decidable≤decidable p23 e = refl
469+ degrade-access-comp decidable≤enum enum≤enum e = refl
470+ degrade-access-comp decidable≤enum enum≤feasible e = refl
471+ degrade-access-comp decidable≤enum enum≤infeasible e = refl
472+ degrade-access-comp decidable≤feasible feasible≤feasible e = refl
473+ degrade-access-comp decidable≤feasible feasible≤infeasible e = refl
474+ degrade-access-comp decidable≤infeasible infeasible≤infeasible e = refl
475+ degrade-access-comp enum≤enum p23 e = refl
476+ degrade-access-comp enum≤feasible feasible≤feasible e = refl
477+ degrade-access-comp enum≤feasible feasible≤infeasible e = refl
478+ degrade-access-comp enum≤infeasible infeasible≤infeasible e = refl
479+ degrade-access-comp feasible≤feasible p23 e = refl
480+ degrade-access-comp feasible≤infeasible infeasible≤infeasible e = refl
481+ degrade-access-comp infeasible≤infeasible infeasible≤infeasible e = refl
482+
483+ -- Factoring-free composition: any direct ordering proof
484+ -- `p13 : c1 ≤a c3` agrees with the composed-via-`c2` degrade, because
485+ -- `≤a-prop` makes the choice of factoring irrelevant. Mirrors
486+ -- `EchoGraded.degrade-compose` and `EchoLinear.degradeMode-compose`.
487+
488+ degrade-access-compose :
489+ ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B}
490+ {c1 c2 c3 : Access}
491+ (p12 : c1 ≤a c2)
492+ (p23 : c2 ≤a c3)
493+ (p13 : c1 ≤a c3)
494+ (e : CEcho c1 f y) →
495+ degrade-access p23 (degrade-access p12 e) ≡ degrade-access p13 e
496+ degrade-access-compose p12 p23 p13 e
497+ rewrite ≤a-prop p13 (≤a-trans p12 p23) = degrade-access-comp p12 p23 e
498+
499+ -- Same composition law restated through the join structure: any
500+ -- degrade to a common upper bound `c` factors through the `c1 ⊔a c2`
501+ -- join. Mirrors `EchoGraded.degrade-via-join` and
502+ -- `EchoLinear.degradeMode-via-join`.
503+
504+ degrade-access-via-join :
505+ ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B}
506+ {c1 c2 c : Access}
507+ (p1 : c1 ≤a c)
508+ (p2 : c2 ≤a c)
509+ (e : CEcho c1 f y) →
510+ degrade-access p1 e
511+ ≡ degrade-access (≤a-⊔a-univ p1 p2) (degrade-access (≤a-⊔a-left c1 c2) e)
512+ degrade-access-via-join {c1 = c1} {c2 = c2} p1 p2 e =
513+ sym (degrade-access-compose (≤a-⊔a-left c1 c2) (≤a-⊔a-univ p1 p2) p1 e)
0 commit comments