|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Gate F4 feasibility spike (docs/echo-types/earn-back-plan.adoc §"Gate |
| 4 | +-- F4 — Universal property, honestly qualified"). |
| 5 | +-- |
| 6 | +-- The R-2026-05-18 retraction narrowed `EchoPullback.echo-pullback-univ` |
| 7 | +-- to a *pointwise* mediator property (`∀ v → m' v ≡ m v`); the |
| 8 | +-- terminal-cone universal property `m' ≡ m` was unstatable there |
| 9 | +-- without funext, and a funext postulate is forbidden estate-wide. |
| 10 | +-- |
| 11 | +-- F4's earn-back is NOT "retracted → unconditional"; it is |
| 12 | +-- "retracted → *true, conditional*": parameterise the strict |
| 13 | +-- terminality result by an EXPLICIT funext hypothesis (a module |
| 14 | +-- parameter — never a postulate), exactly as `Echo.agda` parameterises |
| 15 | +-- `cancel-iso-from-to` / `cancel-iso-to-from` by the triangle-identity |
| 16 | +-- coherences. Then `echo-pullback-univ-strict` is a genuine universal |
| 17 | +-- property *given funext*, with zero postulates retained, and the |
| 18 | +-- unconditional pointwise result stays as the funext-free corollary. |
| 19 | +-- |
| 20 | +-- Result of the spike: it closes in three lines on top of the |
| 21 | +-- already-landed pointwise lemma. No K, no funext in the trusted |
| 22 | +-- base (funext is a hypothesis the caller must supply, exactly like |
| 23 | +-- `triangle₁`/`triangle₂` in `Echo.agda`), zero postulates. Not wired |
| 24 | +-- into `All.agda` / `Smoke.agda` until Gate F4 is recorded passed. |
| 25 | + |
| 26 | +module EchoPullbackUnivF4 where |
| 27 | + |
| 28 | +open import Echo using (Echo) |
| 29 | +open import EchoPullback using (EchoCone; IsMediator; echo-pullback-univ) |
| 30 | +open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) |
| 31 | +open import Relation.Binary.PropositionalEquality using (_≡_) |
| 32 | + |
| 33 | +---------------------------------------------------------------------- |
| 34 | +-- The funext hypothesis, as an explicit (level-0) coherence — NOT a |
| 35 | +-- postulate. `Set₁` because it quantifies over `Set`; this is exactly |
| 36 | +-- the universe `EchoPullback` lives at (`{A B : Set}`, `V : Set`, |
| 37 | +-- `Echo f y : Set`), so no `Setω` and no extra level machinery. |
| 38 | + |
| 39 | +FunExt₀ : Set₁ |
| 40 | +FunExt₀ = |
| 41 | + {A : Set} {B : A → Set} {f g : (x : A) → B x} → |
| 42 | + (∀ x → f x ≡ g x) → f ≡ g |
| 43 | + |
| 44 | +---------------------------------------------------------------------- |
| 45 | +-- Strict terminality, parameterised by funext. |
| 46 | +-- |
| 47 | +-- `echo-cone` is the terminal cone *strictly*: every cone morphism is |
| 48 | +-- equal — as a function — to the mediator, not merely pointwise. The |
| 49 | +-- proof is one application of the supplied `funext` to the pointwise |
| 50 | +-- uniqueness already proved (funext-free, K-free) in |
| 51 | +-- `EchoPullback.echo-pullback-univ`. |
| 52 | + |
| 53 | +module _ (funext : FunExt₀) where |
| 54 | + |
| 55 | + echo-pullback-univ-strict : |
| 56 | + {A B : Set} (f : A → B) (y : B) {V : Set} (c : EchoCone f y V) → |
| 57 | + Σ (V → Echo f y) (λ m → |
| 58 | + IsMediator f y c m |
| 59 | + × (∀ (m' : V → Echo f y) → IsMediator f y c m' → m' ≡ m)) |
| 60 | + echo-pullback-univ-strict f y c with echo-pullback-univ f y c |
| 61 | + ... | m , med , uniq-pt = |
| 62 | + m , med , λ m' med' → funext (uniq-pt m' med') |
| 63 | + |
| 64 | +---------------------------------------------------------------------- |
| 65 | +-- The funext-free corollary is kept verbatim: it is exactly |
| 66 | +-- `EchoPullback.echo-pullback-univ`, re-exported here so the |
| 67 | +-- conditional/unconditional pair lives in one place. Reading: |
| 68 | +-- |
| 69 | +-- * unconditional, zero hypotheses : pointwise mediator property |
| 70 | +-- (`echo-pullback-univ` — `∀ v → m' v ≡ m v`); |
| 71 | +-- * conditional on `funext` : strict terminal cone |
| 72 | +-- (`echo-pullback-univ-strict` — `m' ≡ m`). |
| 73 | +-- |
| 74 | +-- No claim is upgraded beyond what its hypothesis license: the strict |
| 75 | +-- form is *true given funext*, stated as such. |
| 76 | + |
| 77 | +echo-pullback-univ-pointwise : |
| 78 | + {A B : Set} (f : A → B) (y : B) {V : Set} (c : EchoCone f y V) → |
| 79 | + Σ (V → Echo f y) (λ m → |
| 80 | + IsMediator f y c m |
| 81 | + × (∀ (m' : V → Echo f y) → IsMediator f y c m' → |
| 82 | + ∀ v → m' v ≡ m v)) |
| 83 | +echo-pullback-univ-pointwise = echo-pullback-univ |
0 commit comments