|
| 1 | +{-# OPTIONS --cubical --safe #-} |
| 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 | +-- Cubical (REAL) counterpart of `EchoImageFactorizationPropPostulated`. |
| 6 | +-- |
| 7 | +-- ## Purpose |
| 8 | +-- |
| 9 | +-- `EchoImageFactorizationPropPostulated` exhibits the (epi, mono) |
| 10 | +-- image factorisation by ASSUMING propositional truncation `∥_∥` via |
| 11 | +-- four `postulate`s realising `TruncInterface`. Per the estate |
| 12 | +-- Trusted-Base Reduction Policy (`docs/proof-debt.md`) that module is |
| 13 | +-- item (c) "necessary axiom": `∥_∥` cannot be CONSTRUCTED in `--safe |
| 14 | +-- --without-K` without higher inductive types. |
| 15 | +-- |
| 16 | +-- This module DISCHARGES that axiom. In the `--cubical` profile the |
| 17 | +-- propositional truncation is a genuine higher inductive type, so the |
| 18 | +-- four interface obligations become THEOREMS (zero postulates), and |
| 19 | +-- the (epi, mono) factorisation is a real proof rather than a |
| 20 | +-- consequence of assumed laws. `grep postulate` here returns nothing. |
| 21 | +-- |
| 22 | +-- ## Why self-contained (not an import of the `--without-K` base) |
| 23 | +-- |
| 24 | +-- Agda forbids a `--cubical` module from importing a module that is |
| 25 | +-- `--without-K` but not `--cubical-compatible`. The `Echo` kernel |
| 26 | +-- cone (and `EchoImageFactorizationProp`) is `--safe --without-K`, and |
| 27 | +-- re-flagging it to `--cubical-compatible` would change the |
| 28 | +-- kernel-guard funext-free certificate (`scripts/kernel-guard.sh` |
| 29 | +-- Check A greps for the literal `--safe --without-K`). So this module |
| 30 | +-- RESTATES the minimal pieces locally — `TruncInterface`, `Echo`, |
| 31 | +-- `echo-intro`, and the `ImageProp` content — each definitionally |
| 32 | +-- identical to its `--safe --without-K` original. Only the flag |
| 33 | +-- island differs; the mathematical content is the same. |
| 34 | +-- |
| 35 | +-- ## What lands (all postulate-free, `--cubical --safe`) |
| 36 | +-- |
| 37 | +-- * `∥_∥` — the propositional-truncation HIT. |
| 38 | +-- * `is-prop-∥∥`, `rec-∥∥` — the propositionality + recursor, |
| 39 | +-- proved (not assumed): `is-prop-∥∥` is `squash` transported to |
| 40 | +-- the inductive `_≡_`; `rec-∥∥`'s higher-constructor case closes |
| 41 | +-- by the cubical endpoint rule on the converted path. |
| 42 | +-- * `trunc-cubical : TruncInterface ℓ` — the four obligations, |
| 43 | +-- packaged as the SAME record shape the postulated module fakes. |
| 44 | +-- * `module ImagePropCubical f` — the (epi, mono) factorisation |
| 45 | +-- instantiated at `trunc-cubical`: |
| 46 | +-- - `prop-factor-right-injective-real` — MONO side (real). |
| 47 | +-- - `prop-factor-left-mere-surjective-real` — EPI side (real). |
| 48 | +-- |
| 49 | +-- ## Headlines (cubical-lane; see `Cubical/All.agda`) |
| 50 | +-- |
| 51 | +-- * `trunc-cubical` |
| 52 | +-- * `prop-factor-right-injective-real` |
| 53 | +-- * `prop-factor-left-mere-surjective-real` |
| 54 | + |
| 55 | +module EchoImageFactorizationPropCubical where |
| 56 | + |
| 57 | +open import Level using (Level; suc) |
| 58 | +open import Agda.Primitive.Cubical using (i0; primTransp) |
| 59 | +open import Agda.Builtin.Cubical.Path using (PathP) |
| 60 | +open import Data.Product.Base using (Σ; _,_; proj₁) |
| 61 | +open import Relation.Binary.PropositionalEquality |
| 62 | + using (_≡_; refl; cong) |
| 63 | + |
| 64 | +private variable |
| 65 | + ℓ : Level |
| 66 | + |
| 67 | +---------------------------------------------------------------------- |
| 68 | +-- Cubical propositional truncation — the construction the postulates |
| 69 | +-- only asserted |
| 70 | +---------------------------------------------------------------------- |
| 71 | + |
| 72 | +-- homogeneous cubical path (kept distinct from the inductive `_≡_`) |
| 73 | +_≡ᶜ_ : {A : Set ℓ} → A → A → Set ℓ |
| 74 | +_≡ᶜ_ {A = A} x y = PathP (λ _ → A) x y |
| 75 | + |
| 76 | +-- the (-1)-truncation as a higher inductive type |
| 77 | +data ∥_∥ (A : Set ℓ) : Set ℓ where |
| 78 | + inc : A → ∥ A ∥ |
| 79 | + squash : (x y : ∥ A ∥) → x ≡ᶜ y |
| 80 | + |
| 81 | +-- inductive-`≡` ↔ cubical-path, both with definitional endpoints |
| 82 | +eqToPath : {A : Set ℓ} {x y : A} → x ≡ y → x ≡ᶜ y |
| 83 | +eqToPath {x = x} refl = λ _ → x |
| 84 | + |
| 85 | +pathToEq : {A : Set ℓ} {x y : A} → x ≡ᶜ y → x ≡ y |
| 86 | +pathToEq {x = x} p = primTransp (λ i → x ≡ p i) i0 refl |
| 87 | + |
| 88 | +---------------------------------------------------------------------- |
| 89 | +-- The four `TruncInterface` obligations, REAL (no postulates) |
| 90 | +---------------------------------------------------------------------- |
| 91 | + |
| 92 | +-- propositionality: `squash` is a path; transport it to inductive `_≡_` |
| 93 | +is-prop-∥∥ : {A : Set ℓ} (x y : ∥ A ∥) → x ≡ y |
| 94 | +is-prop-∥∥ x y = pathToEq (squash x y) |
| 95 | + |
| 96 | +-- recursion into an inductive-`≡` proposition. The higher-constructor |
| 97 | +-- case lands on a converted path; its `i0`/`i1` boundary reduces to |
| 98 | +-- `rec-∥∥ … x` / `rec-∥∥ … y` definitionally (cubical endpoint rule), |
| 99 | +-- so the clause is well-formed. |
| 100 | +rec-∥∥ : {A B : Set ℓ} → ((x y : B) → x ≡ y) → (A → B) → ∥ A ∥ → B |
| 101 | +rec-∥∥ pB f (inc a) = f a |
| 102 | +rec-∥∥ pB f (squash x y i) = eqToPath (pB (rec-∥∥ pB f x) (rec-∥∥ pB f y)) i |
| 103 | + |
| 104 | +---------------------------------------------------------------------- |
| 105 | +-- `TruncInterface` (local restatement, identical to |
| 106 | +-- `EchoImageFactorizationProp.TruncInterface`) + its REAL instance |
| 107 | +---------------------------------------------------------------------- |
| 108 | + |
| 109 | +record TruncInterface (ℓ : Level) : Set (suc ℓ) where |
| 110 | + field |
| 111 | + Trunc : Set ℓ → Set ℓ |
| 112 | + ∣_∣ : ∀ {A : Set ℓ} → A → Trunc A |
| 113 | + is-prop : ∀ {A : Set ℓ} (x y : Trunc A) → x ≡ y |
| 114 | + rec : ∀ {A B : Set ℓ} |
| 115 | + → ((x y : B) → x ≡ y) |
| 116 | + → (A → B) |
| 117 | + → Trunc A → B |
| 118 | + |
| 119 | +-- the discharge: the postulated `trunc` becomes a real instance |
| 120 | +trunc-cubical : TruncInterface ℓ |
| 121 | +trunc-cubical = record |
| 122 | + { Trunc = ∥_∥ |
| 123 | + ; ∣_∣ = inc |
| 124 | + ; is-prop = is-prop-∥∥ |
| 125 | + ; rec = rec-∥∥ |
| 126 | + } |
| 127 | + |
| 128 | +---------------------------------------------------------------------- |
| 129 | +-- Local `Echo` (definitionally identical to `Echo.Echo`) + intro |
| 130 | +---------------------------------------------------------------------- |
| 131 | + |
| 132 | +Echo : {A B : Set ℓ} → (A → B) → B → Set ℓ |
| 133 | +Echo {A = A} f y = Σ A (λ x → f x ≡ y) |
| 134 | + |
| 135 | +echo-intro : {A B : Set ℓ} (f : A → B) (x : A) → Echo f (f x) |
| 136 | +echo-intro f x = x , refl |
| 137 | + |
| 138 | +---------------------------------------------------------------------- |
| 139 | +-- The (epi, mono) factorisation, parametric in `TruncInterface` |
| 140 | +-- (restated from `EchoImageFactorizationProp.ImageProp`) |
| 141 | +---------------------------------------------------------------------- |
| 142 | + |
| 143 | +module ImageProp {A B : Set ℓ} (T : TruncInterface ℓ) (f : A → B) where |
| 144 | + open TruncInterface T |
| 145 | + |
| 146 | + Image-prop : Set ℓ |
| 147 | + Image-prop = Σ B (λ y → Trunc (Echo f y)) |
| 148 | + |
| 149 | + prop-factor-left : A → Image-prop |
| 150 | + prop-factor-left a = f a , ∣ echo-intro f a ∣ |
| 151 | + |
| 152 | + prop-factor-right : Image-prop → B |
| 153 | + prop-factor-right = proj₁ |
| 154 | + |
| 155 | + prop-factor-commutes : ∀ a → prop-factor-right (prop-factor-left a) ≡ f a |
| 156 | + prop-factor-commutes _ = refl |
| 157 | + |
| 158 | + -- MONO side: the right leg is injective (second component is a prop). |
| 159 | + prop-factor-right-injective : ∀ {z₁ z₂ : Image-prop} |
| 160 | + → prop-factor-right z₁ ≡ prop-factor-right z₂ |
| 161 | + → z₁ ≡ z₂ |
| 162 | + prop-factor-right-injective {b , tr₁} {.b , tr₂} refl = |
| 163 | + cong (b ,_) (is-prop tr₁ tr₂) |
| 164 | + |
| 165 | + -- EPI side: the left leg is mere-surjective onto the image. |
| 166 | + prop-factor-left-mere-surjective : (z : Image-prop) |
| 167 | + → Trunc (Σ A λ a → prop-factor-left a ≡ z) |
| 168 | + prop-factor-left-mere-surjective (b , tr) = |
| 169 | + rec is-prop |
| 170 | + (λ where (a , refl) → ∣ a , cong (f a ,_) (is-prop ∣ echo-intro f a ∣ tr) ∣) |
| 171 | + tr |
| 172 | + |
| 173 | +---------------------------------------------------------------------- |
| 174 | +-- Consumer at the REAL interface + pinned headlines |
| 175 | +---------------------------------------------------------------------- |
| 176 | + |
| 177 | +module ImagePropCubical {A B : Set ℓ} (f : A → B) where |
| 178 | + open ImageProp trunc-cubical f public |
| 179 | + |
| 180 | +prop-factor-right-injective-real : |
| 181 | + ∀ {A B : Set ℓ} (f : A → B) |
| 182 | + {z₁ z₂ : Σ B (λ y → ∥ Echo f y ∥)} |
| 183 | + → ImagePropCubical.prop-factor-right f z₁ |
| 184 | + ≡ ImagePropCubical.prop-factor-right f z₂ |
| 185 | + → z₁ ≡ z₂ |
| 186 | +prop-factor-right-injective-real f = |
| 187 | + ImagePropCubical.prop-factor-right-injective f |
| 188 | + |
| 189 | +prop-factor-left-mere-surjective-real : |
| 190 | + ∀ {A B : Set ℓ} (f : A → B) |
| 191 | + (z : Σ B (λ y → ∥ Echo f y ∥)) |
| 192 | + → ∥ Σ A (λ a → ImagePropCubical.prop-factor-left f a ≡ z) ∥ |
| 193 | +prop-factor-left-mere-surjective-real f = |
| 194 | + ImagePropCubical.prop-factor-left-mere-surjective f |
0 commit comments