EchoImageFactorizationProp — (epi, mono) factorisation module-parameterised in TruncInterface#138
Merged
hyperpolymath merged 5 commits intoMay 28, 2026
Conversation
…erised in TruncInterface
Closes the (epi, mono) earn-back gate that EchoImageFactorization's
preamble flagged. The propositional truncation `∥_∥` is taken as
an explicit module parameter rather than postulated, in the spirit
of the funext-as-module-parameter discipline used in EchoOFSUnivF5
(R-2026-05-18 narrowing).
New module `EchoImageFactorizationProp`:
* `TruncInterface` (record) — packages the four ∥_∥ obligations:
- `Trunc : Set ℓ → Set ℓ`
- `∣_∣ : A → Trunc A`
- `is-prop : ∀ x y → x ≡ y`
- `rec : (B-is-prop) → (A → B) → Trunc A → B`
Any consumer can instantiate with Cubical's `∥_∥₋₁`, a hand-rolled
HIT under different flags, or a postulated interface (consumer's
honest-scope discipline).
* `module ImageProp (T : TruncInterface ℓ) (f : A → B)`:
- `Image-prop := Σ B (λ y → Trunc (Echo f y))` — the (-1)-truncated
image (each fibre collapsed to a prop).
- `prop-factor-left : A → Image-prop` — left leg `a ↦ (f a, ∣ echo-intro a ∣)`.
- `prop-factor-right : Image-prop → B` — right leg = proj₁.
- `prop-factor-commutes` — triangle (definitional).
- `prop-factor-right-injective` — MONO side via `is-prop` on the
truncated second component.
- `prop-factor-left-mere-surjective` — EPI side via `rec` into the
truncated preimage Σ.
## What this proves and does not prove
The factorisation here is the standard (-1)-truncated form: the
right leg is set-injective ("mono"), the left leg is merely
surjective onto the image ("epi" under propositional surjectivity).
The mere-surjectivity + injectivity pair is exactly the (epi, mono)
discipline in the category of sets with propositional truncation.
The (epi, mono) factorisation lands AT the truncation interface; it
does NOT construct the truncation itself. Under the `TruncInterface`
parameter, the proof goes through K-free with zero postulates in
this module.
## Build invariant
* `EchoImageFactorizationProp.agda` compiles standalone under
`--safe --without-K`, zero postulates, no funext. (Local "stdlib
cubical-compat warnings" are unrelated env noise — see
EchoTotalCompletion / Smoke top-level for the same warnings.)
* Wired into `proofs/agda/All.agda` adjacent to
`EchoImageFactorization`, pinned in `proofs/agda/Smoke.agda`
under its own `using` block with header comment.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,193 @@ | |||
| {-# OPTIONS --safe --without-K #-} | |||
🔍 Hypatia Security ScanFindings: 70 issues detected
View findings[
{
"reason": "No test directory or test files found",
"type": "no_tests",
"file": "/home/runner/work/echo-types/echo-types",
"action": "flag",
"rule_module": "honest_completion",
"severity": "high",
"deduction": 20
},
{
"reason": "Issue in secret-scanner.yml",
"type": "missing_workflow",
"file": "secret-scanner.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in governance.yml",
"type": "unknown",
"file": "governance.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in hypatia-scan.yml",
"type": "unknown",
"file": "hypatia-scan.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in mirror.yml",
"type": "unknown",
"file": "mirror.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard.yml",
"type": "unknown",
"file": "scorecard.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/provenance_debugging/ProvenanceDebugging.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/epistemic_erasure/EpistemicErasure.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
🔍 Hypatia Security ScanFindings: 70 issues detected
View findings[
{
"reason": "No test directory or test files found",
"type": "no_tests",
"file": "/home/runner/work/echo-types/echo-types",
"action": "flag",
"rule_module": "honest_completion",
"severity": "high",
"deduction": 20
},
{
"reason": "Issue in secret-scanner.yml",
"type": "missing_workflow",
"file": "secret-scanner.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in governance.yml",
"type": "unknown",
"file": "governance.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in hypatia-scan.yml",
"type": "unknown",
"file": "hypatia-scan.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in mirror.yml",
"type": "unknown",
"file": "mirror.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard.yml",
"type": "unknown",
"file": "scorecard.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/provenance_debugging/ProvenanceDebugging.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/epistemic_erasure/EpistemicErasure.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
…zation-prop-module-param
The new (epi, mono) earn-back module needs an entry in the classification table or kernel-guard.sh Check B fails. Adds it adjacent to EchoImageFactorization in the Tier-2 list, with a one-line annotation in the F5 cohort note explaining it as the truncation-interface earn-back companion. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…://github.com/hyperpolymath/echo-types into session/image-factorization-prop-module-param # Conflicts: # docs/echo-types/echo-kernel-note.adoc
🔍 Hypatia Security ScanFindings: 70 issues detected
View findings[
{
"reason": "No test directory or test files found",
"type": "no_tests",
"file": "/home/runner/work/echo-types/echo-types",
"action": "flag",
"rule_module": "honest_completion",
"severity": "high",
"deduction": 20
},
{
"reason": "Issue in secret-scanner.yml",
"type": "missing_workflow",
"file": "secret-scanner.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in governance.yml",
"type": "unknown",
"file": "governance.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in hypatia-scan.yml",
"type": "unknown",
"file": "hypatia-scan.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in mirror.yml",
"type": "unknown",
"file": "mirror.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard.yml",
"type": "unknown",
"file": "scorecard.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/epistemic_erasure/EpistemicErasure.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/region_exit_audit/RegionExitAudit.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
3 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 28, 2026
…ADME) (#144) ## Summary Surgical narrative refresh across the five canonical doc surfaces (CHANGELOG.md, EXPLAINME.adoc, docs/echo-types/MAP.adoc, README.md, readme.adoc) to catch up with the six PRs that landed 2026-05-28: #136 (kernel-guard fix), #137 (Slice 3 prerequisites), #138 (EchoImageFactorizationProp), #139 (ResidueTaxonomy Search + Epistemic), #140 (banner kit), #141 (Slice 3 headline). ## Changes per file - **CHANGELOG.md** (+78 lines) — new \`### Added (2026-05-28)\` + \`### Fixed (2026-05-28)\` blocks covering all six PRs with honest framing (Slice 3 headline closure described as "under a strict-head premise"; bpsi=bpsi-at-equal-markers caller-burden sub-case explicitly NOT closed). - **EXPLAINME.adoc** (+4 lines) — status-snapshot bullets for Slice 3, canonical identity layer extensions, and CI / foundational hygiene; new \`docs/echo-types/echo-kernel-note.adoc\` entry in "Where to look first". - **docs/echo-types/MAP.adoc** (+14 / -9 net) — new (epi, mono) bullet adjacent to image factorisation; ResidueForm instance count 4 → 6 with Search + Epistemic named; Buchholz proofs list gains RankPowSlice3 + RankPowSlice3Headline with strict-head-premise framing. - **README.md** (+2 / -2) — Tier 1 + Tier 2 mermaid node labels updated for ImageFactorizationProp + Search/Epistemic. - **readme.adoc** (+2 / -1) — Tier 1 + Tier 2 list mirror updated. ## Verification - \`scripts/kernel-guard.sh\` PASS (both Check A funext-free + Check B classification-drift). - No Agda code touched; docs-only refresh. ## Honesty constraints preserved - Slice 3 headline framed as closed *under a strict-head premise*, not unconditionally. - bpsi=bpsi-at-equal-markers caller-burden sub-case explicitly named as NOT closed (rank-adm / rank-lex remaining work). - PR #136 framed as "infrastructure honesty, not a proof-content advance". - 11/13 per-constructor rank-mono count unchanged. ## Test plan - [x] kernel-guard.sh PASS locally - [ ] CI green on this PR - [ ] Admin-merge once green or budget permits 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes the (epi, mono) earn-back gate flagged by
EchoImageFactorization's preamble. The propositional truncation∥_∥is taken as an explicit module parameter rather than postulated, mirroring the funext-as-module-parameter discipline ofEchoOFSUnivF5(R-2026-05-18 narrowing).What lands
New module
EchoImageFactorizationProp:TruncInterface(record) — packages the four∥_∥obligations:Trunc,∣_∣,is-prop,rec. Consumer-pluggable (Cubical's∥_∥₋₁, hand-rolled HIT, or postulated interface).module ImageProp (T : TruncInterface ℓ) (f : A → B)with:Image-prop := Σ B (λ y → Trunc (Echo f y))— the (-1)-truncated imageprop-factor-left/prop-factor-right/prop-factor-commutes— the factorisation legs + triangleprop-factor-right-injective— MONO side viais-propon the truncated second componentprop-factor-left-mere-surjective— EPI side viarecinto the truncated preimage ΣThe mere-surjectivity + injectivity pair is exactly the (epi, mono) discipline in the category of sets with propositional surjectivity.
What this does NOT prove
The (epi, mono) factorisation lands AT the truncation interface; it does NOT construct the truncation itself. Under the
TruncInterfaceparameter, the proof goes through K-free with zero postulates in this module.Build invariant
EchoImageFactorizationProp.agdacompiles standalone under--safe --without-K, zero postulates, no funext.proofs/agda/All.agdaadjacent toEchoImageFactorization, pinned inproofs/agda/Smoke.agdaunder its ownusingblock.Test plan
prop-factor-commutes) is definitional.is-prop; epi side uses onlyrec+is-prop; no funext.