|
2 | 2 |
|
3 | 3 | -- Pillar B (part 1) of docs/echo-types/establishment-plan.adoc. |
4 | 4 | -- |
5 | | --- SCAFFOLD ONLY. Documentation module: no declarations, hence no |
6 | | --- postulates and no holes — it typechecks under `--safe --without-K` |
7 | | --- and is tracked in `All.agda` per the rung-consolidation policy. |
8 | | --- The intended theorems are recorded here as commented specifications |
9 | | --- so a fresh session can start without re-deriving the design. |
| 5 | +-- REAL MODULE (H1 landed 2026-05-17). |
10 | 6 | -- |
11 | 7 | -- Goal: present `Echo f y` as the pullback of `f : A → B` along the |
12 | 8 | -- point `y : ⊤ → B`, and prove its terminal-cone universal property. |
13 | 9 | -- This is the categorical-semantics anchor: it lets a category |
14 | | --- theorist accept echo as a *real object* rather than a notation. |
| 10 | +-- theorist accept echo as a *real object* (the limit of a cospan) |
| 11 | +-- rather than a notation. |
15 | 12 | -- |
16 | | --- Intended signatures (to be filled, in dependency order): |
| 13 | +-- The cospan / pullback square: |
17 | 14 | -- |
18 | | --- -- The pullback square: cone over (f , const y). |
19 | | --- record EchoCone {A B : Set} (f : A → B) (y : B) (V : Set) ... |
| 15 | +-- Echo f y ----proj₁----> A |
| 16 | +-- | | |
| 17 | +-- (! to ⊤) f |
| 18 | +-- | | |
| 19 | +-- v v |
| 20 | +-- ⊤ -------const y---> B |
20 | 21 | -- |
21 | | --- -- Echo is a cone. |
22 | | --- echo-cone : (f : A → B) (y : B) → EchoCone f y (Echo f y) |
| 22 | +-- The ⊤-leg `V → ⊤` is forced (it is constantly `tt`), so a cone over |
| 23 | +-- the cospan with apex `V` is *exactly* a map `p₁ : V → A` together |
| 24 | +-- with the square condition `∀ v → f (p₁ v) ≡ y`. That is precisely an |
| 25 | +-- `EchoCategorical.SliceHom (λ (_ : V) → y) f` — a SliceHom IS a cone, |
| 26 | +-- not merely "in disguise"; the bridge lemmas below make that a |
| 27 | +-- checked fact (round-trips are `refl` by record η). |
23 | 28 | -- |
24 | | --- -- Universal property: any cone factors uniquely through Echo. |
25 | | --- echo-pullback-univ : |
26 | | --- (f : A → B) (y : B) (V : Set) (c : EchoCone f y V) → |
27 | | --- ∃! (λ (m : V → Echo f y) → <cone c factors through echo-cone via m>) |
28 | | --- |
29 | | --- Reuse: `Echo.echo-intro`, `Echo.map-over`, and the existing |
30 | | --- `EchoCategorical.SliceHom` packaging (a SliceHom is already a cone |
31 | | --- morphism in disguise — start by relating the two). |
| 29 | +-- Universal property (terminal cone), stated `--safe --without-K`: |
| 30 | +-- for every cone `c` there is a mediator `m` factoring both legs, and |
| 31 | +-- it is unique *pointwise* among cone morphisms. Uniqueness is stated |
| 32 | +-- pointwise (`∀ v → m' v ≡ m v`), NOT as `m' ≡ m`, so the statement is |
| 33 | +-- funext-free — respecting the establishment-plan funext guardrail. |
| 34 | +-- The second Σ-component is a witness, so the cone-morphism notion |
| 35 | +-- carries the transport-coherence leg `coherent`; this is what makes |
| 36 | +-- uniqueness provable without K (no UIP on `f a ≡ y` is assumed). |
32 | 37 |
|
33 | 38 | module EchoPullback where |
| 39 | + |
| 40 | +open import Echo using (Echo) |
| 41 | +open import EchoCategorical using (SliceHom; arrow; commute) |
| 42 | +open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) |
| 43 | +open import Data.Product.Properties using (Σ-≡,≡→≡) |
| 44 | +open import Relation.Binary.PropositionalEquality |
| 45 | + using (_≡_; refl; subst) |
| 46 | + |
| 47 | +---------------------------------------------------------------------- |
| 48 | +-- Cones over the cospan A --f--> B <--const y-- ⊤. |
| 49 | +-- |
| 50 | +-- The ⊤-leg is forced, so the cone data is just the A-leg plus the |
| 51 | +-- square. Kept at `Set` (level 0): the categorical anchor is cleaner |
| 52 | +-- for a referee without universe noise, and `SliceHom` instantiates |
| 53 | +-- fine at Set₀. |
| 54 | + |
| 55 | +record EchoCone {A B : Set} (f : A → B) (y : B) (V : Set) : Set where |
| 56 | + field |
| 57 | + apex-map : V → A |
| 58 | + square : ∀ v → f (apex-map v) ≡ y |
| 59 | + |
| 60 | +open EchoCone public |
| 61 | + |
| 62 | +-- Echo itself is the canonical cone: proj₁ is the A-leg, proj₂ is the |
| 63 | +-- square. (This is the cone that the universal property is terminal |
| 64 | +-- among.) |
| 65 | +echo-cone : {A B : Set} (f : A → B) (y : B) → EchoCone f y (Echo f y) |
| 66 | +echo-cone f y = record { apex-map = proj₁ ; square = proj₂ } |
| 67 | + |
| 68 | +---------------------------------------------------------------------- |
| 69 | +-- A SliceHom IS a cone (the establishment-plan "in disguise" claim, |
| 70 | +-- now a checked fact). A cone with apex V is exactly a slice morphism |
| 71 | +-- from the constant map `λ (_ : V) → y` to `f`. |
| 72 | + |
| 73 | +cone→slice : |
| 74 | + {A B : Set} {f : A → B} {y : B} {V : Set} → |
| 75 | + EchoCone f y V → SliceHom (λ (_ : V) → y) f |
| 76 | +cone→slice c = record { arrow = apex-map c ; commute = square c } |
| 77 | + |
| 78 | +slice→cone : |
| 79 | + {A B : Set} {f : A → B} {y : B} {V : Set} → |
| 80 | + SliceHom (λ (_ : V) → y) f → EchoCone f y V |
| 81 | +slice→cone h = record { apex-map = arrow h ; square = commute h } |
| 82 | + |
| 83 | +cone→slice→cone : |
| 84 | + {A B : Set} {f : A → B} {y : B} {V : Set} (c : EchoCone f y V) → |
| 85 | + slice→cone (cone→slice c) ≡ c |
| 86 | +cone→slice→cone c = refl |
| 87 | + |
| 88 | +slice→cone→slice : |
| 89 | + {A B : Set} {f : A → B} {y : B} {V : Set} |
| 90 | + (h : SliceHom (λ (_ : V) → y) f) → |
| 91 | + cone→slice (slice→cone h) ≡ h |
| 92 | +slice→cone→slice h = refl |
| 93 | + |
| 94 | +---------------------------------------------------------------------- |
| 95 | +-- Cone morphisms into the canonical Echo cone. |
| 96 | +-- |
| 97 | +-- A morphism from cone `c` (apex V) to `echo-cone` is a map |
| 98 | +-- `m : V → Echo f y` that factors the A-leg (`factor`) and whose |
| 99 | +-- witness, transported along that factoring, recovers the cone's own |
| 100 | +-- square (`coherent`). The `coherent` leg is exactly the Σ-second |
| 101 | +-- coherence that lets uniqueness go through without K. |
| 102 | + |
| 103 | +record IsMediator |
| 104 | + {A B : Set} (f : A → B) (y : B) {V : Set} |
| 105 | + (c : EchoCone f y V) (m : V → Echo f y) : Set where |
| 106 | + field |
| 107 | + factor : ∀ v → proj₁ (m v) ≡ apex-map c v |
| 108 | + coherent : ∀ v → |
| 109 | + subst (λ a → f a ≡ y) (factor v) (proj₂ (m v)) ≡ square c v |
| 110 | + |
| 111 | +open IsMediator public |
| 112 | + |
| 113 | +---------------------------------------------------------------------- |
| 114 | +-- The universal property: `echo-cone` is the terminal cone. |
| 115 | +-- |
| 116 | +-- For every cone `c` there is a mediator `m` (factoring both legs), |
| 117 | +-- and any cone morphism `m'` agrees with `m` pointwise. Existence is |
| 118 | +-- the obvious pairing; uniqueness is one application of stdlib's |
| 119 | +-- `Σ-≡,≡→≡`, fed exactly the `factor`/`coherent` legs — no K, no |
| 120 | +-- funext. |
| 121 | + |
| 122 | +echo-pullback-univ : |
| 123 | + {A B : Set} (f : A → B) (y : B) {V : Set} (c : EchoCone f y V) → |
| 124 | + Σ (V → Echo f y) (λ m → |
| 125 | + IsMediator f y c m |
| 126 | + × (∀ (m' : V → Echo f y) → IsMediator f y c m' → |
| 127 | + ∀ v → m' v ≡ m v)) |
| 128 | +echo-pullback-univ f y c = |
| 129 | + m |
| 130 | + , record { factor = λ _ → refl ; coherent = λ _ → refl } |
| 131 | + , λ m' med v → Σ-≡,≡→≡ (factor med v , coherent med v) |
| 132 | + where |
| 133 | + m : _ → Echo f y |
| 134 | + m v = apex-map c v , square c v |
0 commit comments