|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | +-- SPDX-License-Identifier: MPL-2.0 |
| 3 | +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | + |
| 5 | +-- EchoDisplayed — the displayed-type / fibration packaging of the |
| 6 | +-- categorical base, a faithful Agda mirror of typed-wasm's Idris |
| 7 | +-- `TypedWasm.ABI.Echo` Displayed / DispHom / idDispHom / fromHomOver. |
| 8 | +-- |
| 9 | +-- This module packages the SAME categorical base that `Echo.agda` |
| 10 | +-- already provides (`Echo`, `MapOver`, `map-over`, `map-over-id`, |
| 11 | +-- `map-over-comp`) in the fibrational view that the Idris file carries |
| 12 | +-- but `Echo.agda` does not yet name: |
| 13 | +-- |
| 14 | +-- * `Displayed B` — a displayed type over B (a type family / |
| 15 | +-- fibration `B → Set`). Mirrors Idris `Displayed b = b -> Type`. |
| 16 | +-- * `DispHom p q v` — a morphism of displayed types over a base map |
| 17 | +-- `v : B → B'`: a fibrewise family `p b → q (v b)`. Mirrors the |
| 18 | +-- Idris `record DispHom`. |
| 19 | +-- * `idDispHom p` — the identity displayed morphism over the |
| 20 | +-- identity base. Mirrors Idris `idDispHom`. |
| 21 | +-- * `fromHomOver` — the bridge turning a slice `MapOver` into a |
| 22 | +-- `DispHom` between the two fibre displayed-types over the identity |
| 23 | +-- base. Mirrors Idris `fromHomOver`, which is built from `echoMap` |
| 24 | +-- (= Agda `map-over`). |
| 25 | +-- |
| 26 | +-- HONESTY SCOPE (owner directive). This is PURELY the displayed-type / |
| 27 | +-- fibration packaging of the categorical base. It asserts NOTHING about |
| 28 | +-- variance, and does NOT reintroduce any graded-comonad / |
| 29 | +-- universal-property / model-independence claim — those were RETRACTED; |
| 30 | +-- see docs/retractions.adoc R-2026-05-18. The laws proved here are only: |
| 31 | +-- the identity displayed morphism acts as the identity; `fromHomOver` is |
| 32 | +-- well-defined (its action is exactly `map-over` by construction); and |
| 33 | +-- `fromHomOver` is compatible with the existing `map-over` laws |
| 34 | +-- (identity and composition), all over the identity base. |
| 35 | + |
| 36 | +module EchoDisplayed where |
| 37 | + |
| 38 | +open import Level using (Level; _⊔_; suc) |
| 39 | +open import Function.Base using (_∘_; id) |
| 40 | +open import Data.Product.Base using (Σ; _,_; proj₁; proj₂) |
| 41 | +open import Relation.Binary.PropositionalEquality |
| 42 | + using (_≡_; refl; trans) |
| 43 | + |
| 44 | +open import Echo |
| 45 | + using (Echo; MapOver; map-over; map-over-id; map-over-comp) |
| 46 | + |
| 47 | +---------------------------------------------------------------------- |
| 48 | +-- Displayed types (fibrations / type families) |
| 49 | +-- |
| 50 | +-- Mirrors Idris `Displayed : Type -> Type ; Displayed b = b -> Type`. |
| 51 | +-- We carry an explicit fibre-level `ℓ'` so the fibres may live at any |
| 52 | +-- universe (the Idris version is implicitly large-universe-polymorphic). |
| 53 | + |
| 54 | +Displayed : ∀ {b} (B : Set b) (ℓ' : Level) → Set (b ⊔ suc ℓ') |
| 55 | +Displayed B ℓ' = B → Set ℓ' |
| 56 | + |
| 57 | +---------------------------------------------------------------------- |
| 58 | +-- Morphisms of displayed types over a base map |
| 59 | +-- |
| 60 | +-- Mirrors the Idris |
| 61 | +-- record DispHom (p : Displayed B) (q : Displayed B') (v : B -> B') where |
| 62 | +-- constructor MkDispHom |
| 63 | +-- dispMap : {0 b : B} -> p b -> q (v b) |
| 64 | + |
| 65 | +record DispHom |
| 66 | + {b b' ℓp ℓq} {B : Set b} {B' : Set b'} |
| 67 | + (p : Displayed B ℓp) (q : Displayed B' ℓq) |
| 68 | + (v : B → B') : Set (b ⊔ ℓp ⊔ ℓq) where |
| 69 | + constructor MkDispHom |
| 70 | + field |
| 71 | + dispMap : {x : B} → p x → q (v x) |
| 72 | + |
| 73 | +open DispHom public |
| 74 | + |
| 75 | +---------------------------------------------------------------------- |
| 76 | +-- Identity displayed morphism over the identity base |
| 77 | +-- |
| 78 | +-- Mirrors Idris `idDispHom p = MkDispHom (\x => x)`. |
| 79 | + |
| 80 | +idDispHom : |
| 81 | + ∀ {b ℓp} {B : Set b} (p : Displayed B ℓp) → DispHom p p id |
| 82 | +idDispHom _ = MkDispHom (λ x → x) |
| 83 | + |
| 84 | +---------------------------------------------------------------------- |
| 85 | +-- The fibre of a map, packaged as a displayed type |
| 86 | +-- |
| 87 | +-- Mirrors Idris `EchoOf f = Echo f : Displayed B`. |
| 88 | + |
| 89 | +EchoOf : |
| 90 | + ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → Displayed B (a ⊔ b) |
| 91 | +EchoOf f = Echo f |
| 92 | + |
| 93 | +---------------------------------------------------------------------- |
| 94 | +-- The bridge: a slice MapOver induces a DispHom over the identity base |
| 95 | +-- |
| 96 | +-- Mirrors Idris `fromHomOver h = MkDispHom (\e => echoMap h e)`, where |
| 97 | +-- the Idris `echoMap` is exactly the Agda `map-over` (both transport a |
| 98 | +-- fibre element along a slice morphism over the fixed base). |
| 99 | + |
| 100 | +fromHomOver : |
| 101 | + ∀ {a a' b} {A : Set a} {A' : Set a'} {B : Set b} |
| 102 | + {f : A → B} {f' : A' → B} → |
| 103 | + MapOver f f' → DispHom (EchoOf f) (EchoOf f') id |
| 104 | +fromHomOver m = MkDispHom (λ e → map-over m e) |
| 105 | + |
| 106 | +---------------------------------------------------------------------- |
| 107 | +-- LAWS |
| 108 | +---------------------------------------------------------------------- |
| 109 | + |
| 110 | +-- Law 1. The identity displayed morphism acts as the identity on every |
| 111 | +-- fibre element. (Holds definitionally; pinned as a named theorem.) |
| 112 | +idDispHom-acts-id : |
| 113 | + ∀ {b ℓp} {B : Set b} (p : Displayed B ℓp) |
| 114 | + {x : B} (px : p x) → |
| 115 | + dispMap (idDispHom p) px ≡ px |
| 116 | +idDispHom-acts-id _ _ = refl |
| 117 | + |
| 118 | +-- Law 2. `fromHomOver` is well-defined: its fibrewise action is exactly |
| 119 | +-- the existing `map-over`. This is the compatibility statement that |
| 120 | +-- pins the bridge to the already-verified slice action — there is no |
| 121 | +-- second, divergent definition. (Holds by construction; pinned.) |
| 122 | +fromHomOver-action : |
| 123 | + ∀ {a a' b} {A : Set a} {A' : Set a'} {B : Set b} |
| 124 | + {f : A → B} {f' : A' → B} |
| 125 | + (m : MapOver f f') {y : B} (e : Echo f y) → |
| 126 | + dispMap (fromHomOver {f = f} {f' = f'} m) e ≡ map-over {f = f} {f' = f'} m e |
| 127 | +fromHomOver-action _ _ = refl |
| 128 | + |
| 129 | +-- Law 3. Compatibility of `fromHomOver` with the identity `map-over` |
| 130 | +-- law: the displayed morphism induced by the identity slice morphism |
| 131 | +-- agrees, on every fibre element, with the identity displayed morphism |
| 132 | +-- on the fibre displayed-type. This is `map-over-id` transported across |
| 133 | +-- the bridge. |
| 134 | +fromHomOver-id : |
| 135 | + ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} (e : Echo f y) → |
| 136 | + dispMap (fromHomOver {f = f} {f' = f} (id , (λ x → refl))) e |
| 137 | + ≡ dispMap (idDispHom (EchoOf f)) e |
| 138 | +fromHomOver-id e = map-over-id e |
| 139 | + |
| 140 | +-- Law 4. Compatibility of `fromHomOver` with the composition |
| 141 | +-- `map-over` law. The Idris `DispHom` over the identity base is closed |
| 142 | +-- under fibrewise composition; the bridge sends the composite slice |
| 143 | +-- morphism to the composite of the two induced displayed morphisms, |
| 144 | +-- pointwise on each fibre. This is `map-over-comp` transported across |
| 145 | +-- the bridge (stated on the underlying MapOver Σ-data, matching the way |
| 146 | +-- `map-over-comp` is phrased in `Echo.agda`). |
| 147 | +fromHomOver-comp : |
| 148 | + ∀ {a a' a'' b} |
| 149 | + {A : Set a} {A' : Set a'} {A'' : Set a''} {B : Set b} |
| 150 | + {f : A → B} {f' : A' → B} {f'' : A'' → B} |
| 151 | + (u1 : A → A') (c1 : ∀ x → f' (u1 x) ≡ f x) |
| 152 | + (u2 : A' → A'') (c2 : ∀ x → f'' (u2 x) ≡ f' x) |
| 153 | + {y : B} (e : Echo f y) → |
| 154 | + dispMap (fromHomOver {f = f} {f' = f''} |
| 155 | + (u2 ∘ u1 , (λ x → trans (c2 (u1 x)) (c1 x)))) e |
| 156 | + ≡ dispMap (fromHomOver {f = f'} {f' = f''} (u2 , c2)) |
| 157 | + (dispMap (fromHomOver {f = f} {f' = f'} (u1 , c1)) e) |
| 158 | +fromHomOver-comp u1 c1 u2 c2 e = map-over-comp u1 c1 u2 c2 e |
0 commit comments