Pillar E primer + related work + estate PMPL→MPL-2.0 sweep (harden integration)

[hyperpolymath]

Summary

Brings the harden/ci-flake-pin-2026-05-18 stack onto main, with three logical groupings:

• Harden foundation (P0/P1) — closure-hole closure, external fibre triangulation against stdlib, reproducible CI-via-flake exact pin (additive verifier). These are the earlier commits on the branch; structural work, no Agda regressions.
• Pillar E expansion (commit 8a24530) — clears two [EXPAND] tags on docs/echo-types/paper.adoc:
  • Background and notation primer: 6 subsections (type-theoretic setting, Σ-types + identity, HoTT fibres, coeffect/graded-modality lineage, thin-poset reindexing modalities, notation summary) plus an 18-row notation table whose every symbol is sourced from a real Agda module. Explicit on the post-retraction framing.
  • Related work: 8 per-neighbour subsections (HoTT fibres, graded comonad/coeffect/QTT, lenses/optics, refinement types, setoid quotients, provenance semirings, IFC/modal type theories, synthesis). All <<reframing-note>> xrefs resolve.
  • types-abstract.adoc: per-neighbour related-work positioning block mirroring the paper. Abstract status remains "NOT submission-ready, pending re-review" — content alignment only.
• Licence sweep (commit 2e78761) — collapses the PMPL-1.0-or-later SPDX identifier to MPL-2.0 per owner direction 2026-05-20. 29 source/config files swept; README badge updated; stapeln.toml + arghda-core/Cargo.toml license fields; new docs/PMPL-NARRATIVE.adoc records the cultural/discipline overlay PMPL represented (no legal effect change — MPL-2.0 was already the lawyer-confirmed operative legal effect).

Reconciliation needed before merge

origin/main has advanced by 7 PRs (#64–#70) since this branch's last merge from main:

• docs(bridges): refresh cross-repo bridge status; bake in CNO Agda↔Coq↔Lean4 correspondence #64–bridges(janus): mirror canonical Idris2 OpKind (8-variant) in EchoJanusBridge #66 bridge work (CNO Agda↔Coq↔Lean4 correspondence, EchoTropical correspondence appendix, EchoJanusBridge OpKind mirror — substantive EchoJanusBridge.agda +221 / EchoApprox.agda +132)
• docs: rule out 2-categorical shape; credit landed EchoApprox + EchoDecidable in roadmap #67 docs: rule out 2-categorical shape + roadmap credits
• theory: Axis 8 graded access modality — thin slice (Access, ≤a, ≤a-trans, ≤a-prop) #68 theory: Axis 8 graded access modality (new EchoAccess.agda, 262 lines)
• theory: AntiEcho thin slice — Σ-dual of Echo (carrier + map-over + disjointness) #69 theory: AntiEcho thin slice (new AntiEcho.agda, 93 lines)
• theory: EchoApprox composition rung — first slice (retract direction) #70 theory: EchoApprox composition rung first slice

Expected conflicts (deliberate, owner-resolved):

• paper.adoc — this PR adds Background primer + Related work; parallel sessions may have edited adjacent sections
• types-abstract.adoc — this PR adds a related-work block
• flake.nix — this PR is the full harden-P1 flake; parallel sessions retained the simpler devShell flake
• .github/workflows/*.yml, .machine_readable/6a2/*.a2ml, contractiles/*.a2ml, stapeln.toml, README.md, arghda-core/Cargo.toml, Containerfile, EXPLAINME.adoc, QUICKSTART-*.adoc, TOPOLOGY.adoc, docs/echidna-design-search-2026-04-28.adoc, docs/echo-types/MAP.adoc, docs/echo-types/echo-kernel-note.adoc, scripts/kernel-guard.sh, tools/check-guardrails.sh — licence sweep; conflicts with parallel sessions that kept PMPL headers (resolve by taking this PR's MPL-2.0)

Test plan

• CI green: governance + Agda + Hypatia scans + Scorecard
• flake.nix nix flake check passes (additive verifier)
• agda proofs/agda/All.agda and agda proofs/agda/Smoke.agda both exit 0 under --safe --without-K, zero postulates (no Agda was touched by this branch's recent commits, so this should be a verification-only step)
• AsciiDoc render of paper.adoc — confirm all <<reframing-note>> xrefs resolve
• docs/PMPL-NARRATIVE.adoc reads coherently
• No remaining PMPL/Palimpsest strings outside docs/PMPL-NARRATIVE.adoc + the one intentional pointer in ECOSYSTEM.a2ml

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 10 issues detected

Severity	Count
🔴 Critical	0
🟠 High	5
🟡 Medium	5

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 quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/cache@v4 needs attention",
    "type": "unpinned_action",
    "file": "agda.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "No dependabot.yml or renovate.json found in echo-types",
    "type": "DependencyUpdate",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "high",
    "remediation": "Add .github/dependabot.yml or renovate.json configuration.",
    "scorecard_check": "Dependency-Update-Tool"
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "1 workflow(s) with tag-pinned (not SHA-pinned) actions in echo-types",
    "type": "DependencyPinning",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Pin GitHub Actions and Docker base images by SHA hash.",
    "scorecard_check": "Pinned-Dependencies"
  },
  {
    "reason": "Repository has 1 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence