|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- (Epi, mono) image factorisation — module-parameterised in the |
| 4 | +-- propositional truncation interface. |
| 5 | +-- |
| 6 | +-- Companion to `EchoImageFactorization`. The base module ships the |
| 7 | +-- K-free proof-relevant (equivalence, projection) factorisation |
| 8 | +-- (`Image f := Σ B (Echo f)`); this module degrades it to the |
| 9 | +-- standard set-theoretic (epi, mono) factorisation by truncating |
| 10 | +-- the second component to a proposition. |
| 11 | +-- |
| 12 | +-- The propositional truncation `∥_∥` is taken as an explicit |
| 13 | +-- module-parameter rather than postulated, in the spirit of the |
| 14 | +-- funext-as-module-parameter discipline used in `EchoOFSUnivF5` |
| 15 | +-- (R-2026-05-18 narrowing). Any consumer can instantiate with: |
| 16 | +-- |
| 17 | +-- * Cubical Agda's native `∥_∥₋₁` HIT (once the file's flag profile |
| 18 | +-- allows it), |
| 19 | +-- * a hand-rolled HIT under a different module's relaxed flags, |
| 20 | +-- * a postulated `∥_∥` interface (under the usual honest-scope |
| 21 | +-- discipline; postulates would live in the consumer module). |
| 22 | +-- |
| 23 | +-- This module makes no commitments about how `Trunc` is implemented; |
| 24 | +-- it only consumes the interface laws. |
| 25 | +-- |
| 26 | +-- ## What lands |
| 27 | +-- |
| 28 | +-- * `TruncInterface` — record packaging the four ∥_∥ obligations: |
| 29 | +-- `Trunc`, `∣_∣`, `is-prop`, `rec`. |
| 30 | +-- * `module ImageProp` — module parameterised in |
| 31 | +-- `(T : TruncInterface (a ⊔ b)) (f : A → B)`: |
| 32 | +-- - `Image-prop f := Σ B (λ y → Trunc (Echo f y))` — the |
| 33 | +-- (-1)-truncated image (each fibre collapsed to a prop). |
| 34 | +-- - `prop-factor-left : A → Image-prop f` — left leg. |
| 35 | +-- - `prop-factor-right : Image-prop f → B` — right leg. |
| 36 | +-- - `prop-factor-commutes` — triangle (definitional). |
| 37 | +-- - `prop-factor-right-injective` — mono side: the right leg |
| 38 | +-- is injective (because the second component is a prop). |
| 39 | +-- - `prop-factor-left-mere-surjective` — epi side: every |
| 40 | +-- element of `Image-prop` has a MERE preimage (a `Trunc`-wrapped |
| 41 | +-- Σ). |
| 42 | +-- |
| 43 | +-- ## What this does NOT prove |
| 44 | +-- |
| 45 | +-- The factorisation here is the (-1)-truncated form, which makes |
| 46 | +-- `prop-factor-left` MERELY surjective onto `Image-prop` (not |
| 47 | +-- surjective in the set sense — that would need split surjectivity |
| 48 | +-- which fails for non-decidable predicates). The mere-surjectivity |
| 49 | +-- + injectivity pair is exactly the standard (epi, mono) discipline |
| 50 | +-- in the category of sets with propositional surjectivity as "epi". |
| 51 | +-- |
| 52 | +-- ## Honest scope |
| 53 | +-- |
| 54 | +-- The (epi, mono) factorisation lands AT the truncation interface; |
| 55 | +-- it does not construct the truncation itself. Under the |
| 56 | +-- `TruncInterface` parameter, the proof goes through K-free with |
| 57 | +-- zero postulates inside THIS module. The PROPOSITIONALITY claim |
| 58 | +-- (`prop-factor-right-injective`) requires the interface's |
| 59 | +-- `is-prop` law; the SURJECTIVITY claim |
| 60 | +-- (`prop-factor-left-mere-surjective`) requires the interface's |
| 61 | +-- `rec` eliminator. |
| 62 | +-- |
| 63 | +-- ## Headlines (pin in `Smoke.agda`) |
| 64 | +-- |
| 65 | +-- * `TruncInterface` (record) |
| 66 | +-- * `module ImageProp` (parametric content) |
| 67 | + |
| 68 | +module EchoImageFactorizationProp where |
| 69 | + |
| 70 | +open import Echo using (Echo; echo-intro) |
| 71 | +open import EchoImageFactorization using (Image) |
| 72 | + |
| 73 | +open import Level using (Level; _⊔_; suc) |
| 74 | +open import Data.Product.Base using (Σ; _,_; proj₁; proj₂) |
| 75 | +open import Function.Base using (id; _∘_) |
| 76 | +open import Relation.Binary.PropositionalEquality |
| 77 | + using (_≡_; refl; cong) |
| 78 | + |
| 79 | +private variable |
| 80 | + a b ℓ : Level |
| 81 | + A : Set a |
| 82 | + B : Set b |
| 83 | + |
| 84 | +---------------------------------------------------------------------- |
| 85 | +-- Opaque truncation interface |
| 86 | +---------------------------------------------------------------------- |
| 87 | + |
| 88 | +-- The four obligations every propositional-truncation implementation |
| 89 | +-- must satisfy: |
| 90 | +-- |
| 91 | +-- 1. `Trunc A` exists as a Set at the same level. |
| 92 | +-- 2. Every element of `A` has a (canonical) image in `Trunc A`. |
| 93 | +-- 3. Any two inhabitants of `Trunc A` are equal — this is the |
| 94 | +-- propositionality content (= the "(-1)-truncation"). |
| 95 | +-- 4. To define a function `Trunc A → B` it suffices to give a |
| 96 | +-- function `A → B` together with a proof that `B` is a |
| 97 | +-- proposition — the elimination principle. |
| 98 | +-- |
| 99 | +-- These are independent of any choice of HIT vs postulate; they |
| 100 | +-- characterise propositional truncation up to equivalence. |
| 101 | + |
| 102 | +record TruncInterface (ℓ : Level) : Set (suc ℓ) where |
| 103 | + field |
| 104 | + Trunc : Set ℓ → Set ℓ |
| 105 | + ∣_∣ : ∀ {A : Set ℓ} → A → Trunc A |
| 106 | + is-prop : ∀ {A : Set ℓ} (x y : Trunc A) → x ≡ y |
| 107 | + rec : ∀ {A B : Set ℓ} |
| 108 | + → ((x y : B) → x ≡ y) |
| 109 | + → (A → B) |
| 110 | + → Trunc A → B |
| 111 | + |
| 112 | +---------------------------------------------------------------------- |
| 113 | +-- The (epi, mono) image factorisation, parametric in `TruncInterface` |
| 114 | +---------------------------------------------------------------------- |
| 115 | + |
| 116 | +module ImageProp |
| 117 | + {A : Set ℓ} {B : Set ℓ} |
| 118 | + (T : TruncInterface ℓ) |
| 119 | + (f : A → B) where |
| 120 | + |
| 121 | + open TruncInterface T |
| 122 | + |
| 123 | + -- The (-1)-truncated image: each fibre's existence is collapsed |
| 124 | + -- to a proposition. Distinct echoes at the same `b` collapse to |
| 125 | + -- the same inhabitant of `Image-prop` (so the image really is |
| 126 | + -- "the set of `b`s in the image", not the proof-relevant |
| 127 | + -- `Σ B (Echo f)`). |
| 128 | + Image-prop : Set ℓ |
| 129 | + Image-prop = Σ B (λ y → Trunc (Echo f y)) |
| 130 | + |
| 131 | + -- Left leg: `a ↦ (f a, ∣ echo-intro a ∣)`. |
| 132 | + prop-factor-left : A → Image-prop |
| 133 | + prop-factor-left a = f a , ∣ echo-intro f a ∣ |
| 134 | + |
| 135 | + -- Right leg: project the carrier. |
| 136 | + prop-factor-right : Image-prop → B |
| 137 | + prop-factor-right = proj₁ |
| 138 | + |
| 139 | + -- Triangle: `f ≡ prop-factor-right ∘ prop-factor-left`, |
| 140 | + -- definitional via `proj₁ (f a , _) = f a`. |
| 141 | + prop-factor-commutes : ∀ a → prop-factor-right (prop-factor-left a) ≡ f a |
| 142 | + prop-factor-commutes _ = refl |
| 143 | + |
| 144 | + ---------------------------------------------------------------------- |
| 145 | + -- The MONO side: prop-factor-right is injective |
| 146 | + ---------------------------------------------------------------------- |
| 147 | + |
| 148 | + -- Two inhabitants of `Image-prop` with equal `proj₁`s are equal, |
| 149 | + -- because the second component is a prop (by `is-prop`). This is |
| 150 | + -- exactly the categorical "mono" property in Set. |
| 151 | + -- |
| 152 | + -- The proof unifies the first components via the `refl` premise, |
| 153 | + -- then closes the Σ-equality by `is-prop` on the truncated |
| 154 | + -- second components. K-free under `--without-K`: the unification |
| 155 | + -- is on a fresh-variable position, and the `is-prop` step is |
| 156 | + -- exactly what truncation provides. |
| 157 | + |
| 158 | + prop-factor-right-injective : ∀ {z₁ z₂ : Image-prop} |
| 159 | + → prop-factor-right z₁ ≡ prop-factor-right z₂ |
| 160 | + → z₁ ≡ z₂ |
| 161 | + prop-factor-right-injective {b , tr₁} {.b , tr₂} refl = |
| 162 | + cong (b ,_) (is-prop tr₁ tr₂) |
| 163 | + |
| 164 | + ---------------------------------------------------------------------- |
| 165 | + -- The EPI side: prop-factor-left is mere-surjective |
| 166 | + ---------------------------------------------------------------------- |
| 167 | + |
| 168 | + -- Every element of `Image-prop` has a MERE (truncated) preimage |
| 169 | + -- under `prop-factor-left`. This is the standard (-1)-truncated |
| 170 | + -- surjectivity, which serves as "epi" in Set under propositional |
| 171 | + -- truncation. |
| 172 | + -- |
| 173 | + -- The truncated second component `tr : Trunc (Echo f b)` is |
| 174 | + -- eliminated via `rec` into a `Trunc (Σ A λ a → prop-factor-left a |
| 175 | + -- ≡ z)`. The target is a prop (by `is-prop` on the outer Trunc), |
| 176 | + -- so the eliminator's "respects propositionality" obligation |
| 177 | + -- discharges immediately. |
| 178 | + -- |
| 179 | + -- Inside `rec`, we have `e : Echo f b = (a , p)` where `p : f a ≡ |
| 180 | + -- b`. Then `prop-factor-left a = (f a, ∣echo-intro f a∣)`. To |
| 181 | + -- show `(f a, ∣echo-intro f a∣) ≡ (b, tr)`, we use a Σ-equality: |
| 182 | + -- the first components are unified by `p : f a ≡ b`, and the |
| 183 | + -- second components are both `Trunc (Echo f b)` so equal by |
| 184 | + -- `is-prop`. The resulting witness is wrapped in `∣_∣` to land |
| 185 | + -- in `Trunc (Σ ...)`. |
| 186 | + |
| 187 | + prop-factor-left-mere-surjective : (z : Image-prop) |
| 188 | + → Trunc (Σ A λ a → prop-factor-left a ≡ z) |
| 189 | + prop-factor-left-mere-surjective (b , tr) = |
| 190 | + rec is-prop |
| 191 | + (λ where |
| 192 | + (a , refl) → ∣ a , cong (f a ,_) (is-prop ∣ echo-intro f a ∣ tr) ∣) |
| 193 | + tr |
0 commit comments