|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 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 | +-- Echo↔Ephapax L3 Bridge (NARROW — navigability + cross-repo cataloguing). |
| 6 | +-- |
| 7 | +-- The ephapax programming-language project (hyperpolymath/ephapax) |
| 8 | +-- carries a four-layer typing redesign whose L3 layer (`formal/Echo.v`, |
| 9 | +-- 584 lines, 24 `Qed`, zero `Admitted` / zero `Axiom`) is an explicit |
| 10 | +-- Coq port of `EchoLinear.agda` + `EchoResidue.agda` under a K-free / |
| 11 | +-- zero-axiom discipline equivalent to `--safe --without-K`. The Coq |
| 12 | +-- headlines `mode_le_prop`, `weaken_collapses_distinction`, |
| 13 | +-- `affine_canonical`, `degrade_mode_comp`, and |
| 14 | +-- `no_section_collapse_to_residue` each carry the same theorem as the |
| 15 | +-- Agda counterpart pinned here. |
| 16 | +-- |
| 17 | +-- Scope (NARROW, per `/tmp/ephapax-bridge-proposal.md` §4): this |
| 18 | +-- module is import-time documentation. The cross-repo content |
| 19 | +-- correspondence is already discharged by `coqc` on the ephapax side |
| 20 | +-- (no Lane 4 CI dependency). The two definitional `refl`-renames |
| 21 | +-- below pin the load-bearing Agda symbols under `ephapax-`-prefixed |
| 22 | +-- names so `MAP.adoc`'s "Directions" navigation has an ephapax row, |
| 23 | +-- and so a silent upstream rename trips `Smoke.agda`. A future |
| 24 | +-- content bridge would require an Agda mirror of ephapax's |
| 25 | +-- `formal/Echo.v` and is not foreclosed by this stub. |
| 26 | +-- |
| 27 | +-- References: |
| 28 | +-- * `docs/bridges/cross-repo-bridge-status.md` (when extended). |
| 29 | +-- * `docs/echo-types/MAP.adoc` §"Directions" / "Ephapax L3". |
| 30 | +-- * ephapax `formal/Echo.v:502-517` ↔ |
| 31 | +-- `EchoResidue.no-section-collapse-to-residue`. |
| 32 | +-- * ephapax `formal/Echo.v` `weaken` ↔ `EchoLinear.weaken`. |
| 33 | + |
| 34 | +module EchoEphapaxBridge where |
| 35 | + |
| 36 | +open import EchoLinear using (linear; affine; LEcho; weaken) |
| 37 | +open import EchoResidue using (no-section-collapse-to-residue) |
| 38 | + |
| 39 | +-- ephapax `formal/Echo.v` `weaken` — Coq port of this Agda symbol. |
| 40 | +ephapax-L3-weaken : LEcho linear → LEcho affine |
| 41 | +ephapax-L3-weaken = weaken |
| 42 | + |
| 43 | +-- ephapax `formal/Echo.v` `no_section_collapse_to_residue` |
| 44 | +-- (line 502-517, `Qed`, zero axioms) — Coq port of this Agda symbol. |
| 45 | +ephapax-L3-no-section-collapse = no-section-collapse-to-residue |
0 commit comments