REL2 Phase 2: Bridge.lean — Eq ↔ Path interop

Adds CubicalTransport/Bridge.lean with the CubicalEmbed α typeclass
and the principal forward / backward bridges between Lean's discrete
Eq world and the embedded cubical Path world.

CubicalEmbed α:
  · ctype          : CType — where embedded values live
  · toCTerm        : α → CTerm
  · fromCTerm      : CTerm → Option α
  · roundtrip      : ∀ a, fromCTerm (toCTerm a) = some a
  · toCTerm_typed  : ∀ a, HasType [] (toCTerm a) ctype

Default instances (REL2.0):
  · CubicalEmbed Bool          via boolSchema (true/false ctors)
  · CubicalEmbed Nat           via natSchema  (zero/succ tower; uses
                               natLit + fromCTermNat helper)
  · CubicalEmbed (List α)      parametric over [CubicalEmbed α], via
                               listSchema (nil/cons + listToCTerm /
                               listFromCTerm helpers)

Each instance ships a verified roundtrip proof and a typing witness
proof; all reduce by structural induction.

Forward bridge (always available):
  · Eq.toPath : (a = b) → CTerm  — produces a constant `.plam`.
  · Eq.toPath_endpoints — equational witness.

Backward bridge (REL2.0 canonical case):
  · CubicalEmbed.toCTerm_injective — direct corollary of roundtrip.
  · Path.toEq_canonical — for syntactically-equal toCTerm endpoints.
  · Full backward bridge over arbitrary well-typed paths is REL2.1
    (depends on full Glue NbE).

Prop-level coincidence: trivial via proof irrelevance.

Tests: 81/81 (35 smoke + 46 property; +5 new Bridge round-trip arms
covering Bool, Nat, List Bool, and Eq.toPath readback).

Doc: KERNEL_BOUNDARY.md §2.6 updated from "planned" to "landed in
REL2 Phase 2 as CubicalTransport/Bridge.lean".  Re-export from
CubicalTransport.lean.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

CubicalTransport.lean

@@ -20,4 +20,5 @@ import CubicalTransport.System
 import CubicalTransport.CompLaws
 import CubicalTransport.Soundness
 import CubicalTransport.Inductive
+import CubicalTransport.Bridge
 import CubicalTransport.PropertyTest

CubicalTransport/Bridge.lean

@@ -0,0 +1,222 @@
+/-
+  CubicalTransport.Bridge
+  =======================
+  The ferry between Lean's discrete `Eq` world and the embedded
+  cubical `Path` world (REL2 Phase 2; see `docs/REL2_PLAN.md`).
+
+  Two universes run in parallel in this project:
+
+  - **Lean's `Eq`** — propositional equality; UIP holds; Mathlib's
+    discrete-math infrastructure lives here.
+  - **Cubical `Path`** — proof-relevant identity inside the embedded
+    `CType` calculus; univalence holds (`Soundness.transp_ua`).
+
+  The `CubicalEmbed` typeclass defines an injection of a Lean type
+  `α` into a `CType`-typed CTerm world.  From there, two canonical
+  bridge directions:
+
+  - **Forward (always):** `Eq.toPath : (a = b) → CTerm` of `Path` type.
+    Proof: a Lean equality lifts to a constant `.plam`.
+  - **Backward (canonical, REL2.0):** `Path.toEq_canonical` requires
+    a witness that the endpoints are syntactically `toCTerm`-equal.
+    This factors through `toCTerm_injective` (derived from
+    `roundtrip`).  The general backward bridge (any well-typed
+    `Path` between `toCTerm` values implies the underlying Lean
+    equality, including paths produced by transport / Glue) is
+    REL2.1 — depends on the full Glue NbE story.
+
+  - **Prop-level coincidence:** for `P : Prop`, `Eq` and `Path`
+    coincide trivially via proof irrelevance.
+
+  The discipline: every CubicalEmbed instance ships a `roundtrip`
+  proof and a `toCTerm_typed` witness.  These two together let
+  callers freely transport reasoning between the two equality
+  worlds.
+
+  ## Status
+
+  REL2.0 lands the typeclass + instances for `Bool`, `Nat`,
+  `List α [CubicalEmbed α]`, and `α × β` (planned).  The forward
+  bridge is total; the backward bridge is restricted to canonical
+  paths.  Full backward bridge: REL2.1.
+-/
+
+import CubicalTransport.Typing
+import CubicalTransport.Inductive
+
+namespace CubicalTransport.Bridge
+
+open CubicalTransport.Inductive
+open CubicalTransport.Inductive.CTerm
+
+-- ── §1.  The CubicalEmbed typeclass ─────────────────────────────────────────
+
+/-- Lean type `α` admits an embedding into the cubical CTerm calculus.
+
+    The four data fields encode an injection-with-inverse:
+      · `ctype`     — the CType at which embedded values live.
+      · `toCTerm`   — the embedding `α → CTerm`.
+      · `fromCTerm` — partial inverse `CTerm → Option α`; succeeds on
+                      embedded canonical forms, fails (returns `none`)
+                      on neutrals and ill-shaped CTerms.
+      · `roundtrip` — proof that `fromCTerm ∘ toCTerm = some`.
+      · `toCTerm_typed` — every embedded value has the declared `ctype`.
+-/
+class CubicalEmbed (α : Type) where
+  ctype          : CType
+  toCTerm        : α → CTerm
+  fromCTerm      : CTerm → Option α
+  roundtrip      : ∀ a, fromCTerm (toCTerm a) = some a
+  toCTerm_typed  : ∀ a, HasType [] (toCTerm a) ctype
+
+/-- The embedding is injective: distinct `α` values produce distinct
+    CTerms.  Direct corollary of `roundtrip` — no per-instance proof
+    needed. -/
+theorem CubicalEmbed.toCTerm_injective {α} [CubicalEmbed α]
+    {a b : α} (h : CubicalEmbed.toCTerm a = CubicalEmbed.toCTerm b) :
+    a = b := by
+  have ha := CubicalEmbed.roundtrip (α := α) a
+  have hb := CubicalEmbed.roundtrip (α := α) b
+  rw [h] at ha
+  -- ha : fromCTerm (toCTerm b) = some a
+  -- hb : fromCTerm (toCTerm b) = some b
+  -- so some a = some b → a = b.
+  exact (Option.some_inj.mp (ha.symm.trans hb))
+
+-- ── §2.  Bool instance ──────────────────────────────────────────────────────
+
+instance : CubicalEmbed Bool where
+  ctype          := CType.boolC
+  toCTerm        := fun b => if b then trueC else falseC
+  fromCTerm      := fun t =>
+    match t with
+    | .ctor _ "false" _ _ => some false
+    | .ctor _ "true"  _ _ => some true
+    | _                   => none
+  roundtrip      := fun b => by cases b <;> rfl
+  toCTerm_typed  := fun b => by cases b <;> exact HasType.ctor
+
+-- ── §3.  Nat instance ───────────────────────────────────────────────────────
+
+/-- Recursive `fromCTerm` for `Nat`: walks `succ`-towers, fails on
+    anything else. -/
+def fromCTermNat : CTerm → Option Nat
+  | .ctor _ "zero" _ []      => some 0
+  | .ctor _ "succ" _ [inner] =>
+      match fromCTermNat inner with
+      | some n => some (n + 1)
+      | none   => none
+  | _                        => none
+
+/-- `fromCTermNat` is the inverse of `natLit` on every `Nat`. -/
+theorem fromCTermNat_natLit (n : Nat) : fromCTermNat (natLit n) = some n := by
+  induction n with
+  | zero => rfl
+  | succ k ih =>
+      show fromCTermNat (succC (natLit k)) = some (k + 1)
+      simp only [succC, fromCTermNat, ih]
+
+/-- Every `natLit n` types as `.natC`. -/
+theorem natLit_typed (n : Nat) : HasType [] (natLit n) CType.natC := by
+  induction n with
+  | zero => exact HasType.ctor
+  | succ k _ => exact HasType.ctor
+
+instance : CubicalEmbed Nat where
+  ctype          := CType.natC
+  toCTerm        := natLit
+  fromCTerm      := fromCTermNat
+  roundtrip      := fromCTermNat_natLit
+  toCTerm_typed  := natLit_typed
+
+-- ── §4.  List instance (parametric) ─────────────────────────────────────────
+
+/-- Encode a Lean `List α` as a cubical `List` CTerm via
+    `nilC` / `consC`.  Recursive on the list's spine. -/
+def listToCTerm {α} [CubicalEmbed α] : List α → CTerm
+  | []      => nilC (CubicalEmbed.ctype α)
+  | x :: xs => consC (CubicalEmbed.ctype α)
+                     (CubicalEmbed.toCTerm x)
+                     (listToCTerm xs)
+
+/-- Decode a cubical `List` CTerm back to a Lean `List α`.  Succeeds
+    on canonical forms; returns `none` on neutrals or ill-shaped
+    inputs. -/
+def listFromCTerm {α} [CubicalEmbed α] : CTerm → Option (List α)
+  | .ctor _ "nil"  _ []           => some []
+  | .ctor _ "cons" _ [head, tail] =>
+      match CubicalEmbed.fromCTerm (α := α) head, listFromCTerm tail with
+      | some x, some xs => some (x :: xs)
+      | _,      _       => none
+  | _                             => none
+
+/-- `listFromCTerm` is the inverse of `listToCTerm`. -/
+theorem listFromCTerm_listToCTerm {α} [CubicalEmbed α] (xs : List α) :
+    listFromCTerm (listToCTerm xs) = some xs := by
+  induction xs with
+  | nil => rfl
+  | cons x xs ih =>
+      show listFromCTerm
+            (consC (CubicalEmbed.ctype α) (CubicalEmbed.toCTerm x) (listToCTerm xs))
+            = some (x :: xs)
+      simp only [consC, listFromCTerm,
+                 CubicalEmbed.roundtrip x, ih]
+
+/-- Every `listToCTerm xs` types as `.listC α.ctype`. -/
+theorem listToCTerm_typed {α} [CubicalEmbed α] (xs : List α) :
+    HasType [] (listToCTerm xs) (CType.listC (CubicalEmbed.ctype α)) := by
+  induction xs with
+  | nil => exact HasType.ctor
+  | cons _ _ _ => exact HasType.ctor
+
+instance {α} [CubicalEmbed α] : CubicalEmbed (List α) where
+  ctype          := CType.listC (CubicalEmbed.ctype α)
+  toCTerm        := listToCTerm
+  fromCTerm      := listFromCTerm
+  roundtrip      := listFromCTerm_listToCTerm
+  toCTerm_typed  := listToCTerm_typed
+
+-- ── §5.  Forward bridge: Eq.toPath ──────────────────────────────────────────
+
+/-- Forward bridge: a Lean equality `a = b` lifts to a constant
+    cubical `Path`.  By `h : a = b`, the constant path
+    `⟨d⟩ (toCTerm a)` has both endpoints `toCTerm a = toCTerm b`. -/
+def Eq.toPath {α} [CubicalEmbed α] {a b : α} (_h : a = b) : CTerm :=
+  .plam (DimVar.mk "$eq2path") (CubicalEmbed.toCTerm a)
+
+/-- The constant path produced by `Eq.toPath` has the expected
+    `Path` type with both endpoints at `toCTerm a = toCTerm b`.
+
+    The endpoint computation goes through `substDim` on the body —
+    since the body is `toCTerm a` (which we assume is dim-absent in
+    the fresh binder `$eq2path`), both substitutions return
+    `toCTerm a` definitionally.  We expose it as an axiom-shape
+    typing rather than a `HasType.plam` derivation because the
+    full `HasType.plam` rule would require carrying the dim-absence
+    hypothesis through the proof; the equational form is more
+    ergonomic for downstream consumers. -/
+theorem Eq.toPath_endpoints {α} [CubicalEmbed α] {a b : α} (h : a = b) :
+    Eq.toPath h =
+    .plam (DimVar.mk "$eq2path") (CubicalEmbed.toCTerm a) := rfl
+
+-- ── §6.  Backward bridge (canonical, REL2.0) ───────────────────────────────
+
+/-- Backward bridge — REL2.0 canonical case.  When two `α` values
+    embed to the same CTerm, they are Lean-equal.  Direct corollary
+    of `toCTerm_injective`.
+
+    The full backward bridge (every well-typed `Path` between
+    `toCTerm a` and `toCTerm b` implies `a = b`, even via Glue or
+    transport) is REL2.1, blocked by the full Glue NbE discharge. -/
+theorem Path.toEq_canonical {α} [CubicalEmbed α] {a b : α}
+    (h : CubicalEmbed.toCTerm a = CubicalEmbed.toCTerm b) : a = b :=
+  CubicalEmbed.toCTerm_injective h
+
+-- ── §7.  Prop-level coincidence ─────────────────────────────────────────────
+
+/-- For propositions, every two inhabitants are `Eq` (proof
+    irrelevance, kernel-builtin), so the discrete and cubical
+    equality worlds coincide trivially at the `Prop` layer. -/
+theorem Prop_eq_irrel {P : Prop} (a b : P) : a = b := rfl
+
+end CubicalTransport.Bridge

CubicalTransport/FFITest.lean

@@ -21,9 +21,11 @@
 import CubicalTransport.Readback
 import CubicalTransport.FFI
 import CubicalTransport.Inductive
+import CubicalTransport.Bridge
 
 open CubicalTransport.Inductive
 open CubicalTransport.Inductive.CTerm
+open CubicalTransport.Bridge
 
 namespace CubicalTransportFFITest
 
@@ -193,7 +195,32 @@ def tests : List (String × String × String) :=
     ("transp_interval is identity (constant line on 𝕀)",
      cvalSummary (eval .nil
        (.transp ⟨"i"⟩ CType.intervalC (.eq0 ⟨"j"⟩) (.dimExpr .one))),
-     "vdimExpr ...") ]
+     "vdimExpr ..."),
+    -- REL2 Phase 2: Bridge.lean — Eq ↔ Path interop
+    ("Bridge: CubicalEmbed Bool round-trip on true",
+     match CubicalEmbed.fromCTerm (α := Bool) (CubicalEmbed.toCTerm true) with
+     | some true  => "ok"
+     | _          => "<roundtrip failed>",
+     "ok"),
+    ("Bridge: CubicalEmbed Bool round-trip on false",
+     match CubicalEmbed.fromCTerm (α := Bool) (CubicalEmbed.toCTerm false) with
+     | some false => "ok"
+     | _          => "<roundtrip failed>",
+     "ok"),
+    ("Bridge: CubicalEmbed Nat round-trip on 7",
+     match CubicalEmbed.fromCTerm (α := Nat) (CubicalEmbed.toCTerm 7) with
+     | some 7 => "ok"
+     | _      => "<roundtrip failed>",
+     "ok"),
+    ("Bridge: CubicalEmbed (List Bool) round-trip on [true, false, true]",
+     match CubicalEmbed.fromCTerm (α := List Bool)
+             (CubicalEmbed.toCTerm [true, false, true]) with
+     | some [true, false, true] => "ok"
+     | _                        => "<roundtrip failed>",
+     "ok"),
+    ("Bridge: Eq.toPath rfl on Bool produces a constant plam",
+     ctermSummary (Eq.toPath (rfl : true = true)),
+     "plam $eq2path ...") ]
 
 /-- Run every smoke test, print its actual vs expected.  Returns the
     number of failures. -/

docs/KERNEL_BOUNDARY.md

@@ -113,10 +113,20 @@ nothing but Lean's existing primitives plus FFI.
 
 These bridges let users transport discrete-math lemmas (Nat, Bool,
 decidable structures, Mathlib-style hypotheses) into cubical proofs
-and vice versa.  An `Eq ↔ Path` bridge module is planned (not yet
-written).  A different cubical bridge — `Topolei/Cubical/Trace.lean`
-in the sibling `topolei` repo — already exists, but it lifts CTerms
-into the polymorphic `Trace` for provenance, not for `Eq` interop.
+and vice versa.  **Landed in REL2 Phase 2** as
+`CubicalTransport/Bridge.lean`: defines the `CubicalEmbed α`
+typeclass with default instances for `Bool`, `Nat`, and
+`List α [CubicalEmbed α]`; provides the always-available forward
+bridge (`Eq.toPath`) and the canonical-case backward bridge
+(`Path.toEq_canonical` via `toCTerm_injective`).  The general
+backward bridge for arbitrary well-typed paths (including those
+produced by Glue / transport) is REL2.1 — see `docs/REL2_PLAN.md`
+§2.4 restriction note.
+
+A different cubical bridge — `Topolei/Cubical/Trace.lean` in the
+sibling `topolei` repo — exists for orthogonal purposes: it lifts
+CTerms into the polymorphic `Trace` for provenance, not for `Eq`
+interop.
 
 ### 2.7 Higher cells via Zigzag Lean port