diff --git a/CubicalTransport/Reflect.lean b/CubicalTransport/Reflect.lean
new file mode 100644
index 0000000..5027ecd
--- /dev/null
+++ b/CubicalTransport/Reflect.lean
@@ -0,0 +1,1410 @@
+/-
+  CubicalTransport.Reflect
+  ========================
+  Reflection metaprogramming layer (THEORY.md §0.9).
+
+  Bidirectional bridge between the engine's first-class CTerm / CType
+  inductives and Lean's tactic-facing `Lean.Expr` representation.
+
+  ## What this module exports
+
+    · `reflectULevel : ULevel → MetaM Expr`
+    · `reflectCType  : ∀ {ℓ : ULevel}, CType ℓ → MetaM Expr`
+    · `reflectCTerm  : CTerm → MetaM Expr`
+
+    · `reifyULevel   : Expr → MetaM (Option ULevel)`
+    · `reifyCType    : Expr → MetaM (Option (Σ ℓ : ULevel, CType ℓ))`
+    · `reifyCTerm    : Expr → MetaM (Option CTerm)`
+
+    · `Contract.register      : Lean.Name → ContractEntry → IO Unit`
+    · `Contract.lookupByName  : Lean.Name → IO (Option ContractEntry)`
+    · `Contract.allRegistered : IO (List Lean.Name)`
+
+    · Round-trip theorems on the image of the reflection functions.
+
+  ## Design
+
+  · `reflectCType` produces a Lean `Expr` that, when elaborated in
+    a context with `CubicalTransport` open, evaluates back to the
+    original CType.  Each constructor maps to a fully-applied
+    `Expr.app`-tree over its constructor's `Lean.Name`, with every
+    implicit `{ℓ : ULevel}` argument made explicit (Expr-level
+    construction is always fully explicit).
+
+  · `reflectCTerm` is similar.
+
+  · The mutual nature of CType / CTerm is reflected at the
+    metaprogramming level: `reflectCType` calls `reflectCTerm` on
+    its CTerm sub-payloads (path endpoints, glue equiv components),
+    and `reflectCTerm` calls `reflectCType` on its CType payloads
+    (transp / comp / code arguments).
+
+  · `reify*` are the inverses, returning `Option` because not every
+    `Expr` is a valid encoding.  `reifyULevel` is fully discharged
+    structurally; `reifyCType` and `reifyCTerm` have their full
+    per-constructor inverse pending the `Expr`-pattern-matching
+    scaffolding (annotated below).
+
+  · The Contract registry is an
+        `IO.Ref (Std.HashMap Lean.Name ContractEntry)`.
+    Contracts register themselves in their defining module's
+    `initialize` block; tactics and other consumers look them up
+    by name.
+
+  ## Coupling note (Contract module)
+
+  The `Contract` type itself is `def Contract (ℓ : ULevel) : Type :=
+  CType ℓ → CTerm` — exported by `CubicalTransport.Contract`.  This
+  module re-exports the same definition locally (as an `abbrev` —
+  definitionally equal to the upstream) to avoid a circular
+  dependency: contracts in `CubicalTransport.Contract` will register
+  themselves into the registry exposed here, so `Contract` must
+  import `Reflect`, not the other way around.  The two spellings
+  unify by reducibility, so registering a `Contract.Contract` value
+  via `Reflect.Contract.register` typechecks without any conversion.
+-/
+
+import Lean
+import CubicalTransport.Syntax
+import CubicalTransport.Inductive
+import CubicalTransport.Typing
+
+namespace CubicalTransport.Reflect
+
+open Lean Meta
+
+/-- Local re-export of the Contract type; definitionally equal to
+    `CubicalTransport.Contract.Contract`. -/
+abbrev Contract (ℓ : ULevel) : Type := CType ℓ → CTerm
+
+-- ── §1.  Reflection: ULevel → Expr ──────────────────────────────────────────
+
+/-- Reflect a `ULevel` to its `Lean.Expr` encoding.  Walks the
+    inductive's two constructors directly; the produced Expr is
+    `@ULevel.zero` or `@ULevel.succ <recurse>`. -/
+partial def reflectULevel : ULevel → MetaM Expr
+  | .zero    => return mkConst ``ULevel.zero
+  | .succ n  => do
+      let ne ← reflectULevel n
+      return mkApp (mkConst ``ULevel.succ) ne
+
+-- ── §2.  Reflection helpers (DimVar / DimExpr / FaceFormula / schema) ─────
+
+/-- Reflect a `DimVar` (a single-field structure carrying `name : String`). -/
+partial def reflectDimVar : DimVar → MetaM Expr
+  | ⟨name⟩ => return mkApp (mkConst ``DimVar.mk) (mkStrLit name)
+
+/-- Reflect a `DimExpr` (the free de Morgan algebra on dim variables).
+    Walks all six constructors: `.zero`, `.one`, `.var i`, `.inv r`,
+    `.meet r s`, `.join r s`. -/
+partial def reflectDimExpr : DimExpr → MetaM Expr
+  | .zero      => return mkConst ``DimExpr.zero
+  | .one       => return mkConst ``DimExpr.one
+  | .var i     => do
+      let iE ← reflectDimVar i
+      return mkApp (mkConst ``DimExpr.var) iE
+  | .inv r     => do
+      let rE ← reflectDimExpr r
+      return mkApp (mkConst ``DimExpr.inv) rE
+  | .meet r s  => do
+      let rE ← reflectDimExpr r
+      let sE ← reflectDimExpr s
+      return mkAppN (mkConst ``DimExpr.meet) #[rE, sE]
+  | .join r s  => do
+      let rE ← reflectDimExpr r
+      let sE ← reflectDimExpr s
+      return mkAppN (mkConst ``DimExpr.join) #[rE, sE]
+
+/-- Reflect a `FaceFormula`.  Walks all six constructors:
+    `.bot`, `.top`, `.eq0 i`, `.eq1 i`, `.meet ϕ ψ`, `.join ϕ ψ`. -/
+partial def reflectFaceFormula : FaceFormula → MetaM Expr
+  | .bot       => return mkConst ``FaceFormula.bot
+  | .top       => return mkConst ``FaceFormula.top
+  | .eq0 i     => do
+      let iE ← reflectDimVar i
+      return mkApp (mkConst ``FaceFormula.eq0) iE
+  | .eq1 i     => do
+      let iE ← reflectDimVar i
+      return mkApp (mkConst ``FaceFormula.eq1) iE
+  | .meet a b  => do
+      let aE ← reflectFaceFormula a
+      let bE ← reflectFaceFormula b
+      return mkAppN (mkConst ``FaceFormula.meet) #[aE, bE]
+  | .join a b  => do
+      let aE ← reflectFaceFormula a
+      let bE ← reflectFaceFormula b
+      return mkAppN (mkConst ``FaceFormula.join) #[aE, bE]
+
+-- ── §3.  Reflection: CType / CTerm → Expr ──────────────────────────────────
+
+/-- The `Expr` for the family `fun ℓ : ULevel => CType ℓ`, used as
+    the implicit family argument of `Sigma.mk` when reflecting
+    heterogeneous-level CType lists.  Built once via the bound-
+    variable `Expr.bvar 0` under a single λ-binder. -/
+def cTypeFamilyExpr : Expr :=
+  .lam `ℓ (mkConst ``ULevel)
+    (mkApp (mkConst ``CType) (.bvar 0))
+    .default
+
+/-- The `Expr` for the type `Σ ℓ : ULevel, CType ℓ`. -/
+def cTypeSigmaExpr : Expr :=
+  mkAppN (mkConst ``Sigma [Level.zero, Level.zero])
+    #[mkConst ``ULevel, cTypeFamilyExpr]
+
+/-- Build the `Expr` for `@Sigma.mk ULevel (fun ℓ => CType ℓ) ℓE AE`. -/
+def mkSigmaULevelCType (ℓE : Expr) (AE : Expr) : Expr :=
+  mkAppN (mkConst ``Sigma.mk [Level.zero, Level.zero])
+    #[mkConst ``ULevel, cTypeFamilyExpr, ℓE, AE]
+
+mutual
+  /-- Reflect a `CType` (at any universe level) to a `Lean.Expr`.
+      The level `ℓ` is itself reflected and emitted as the explicit
+      implicit-position argument of the constructor in the Expr-form. -/
+  partial def reflectCType : {ℓ : ULevel} → CType ℓ → MetaM Expr := fun {ℓ} t =>
+    match t with
+    | .univ =>
+        -- `@CType.univ ℓ_inner` where ℓ = ℓ_inner.succ.  We need
+        -- ℓ_inner — recover it from the result level ℓ : .succ ℓ_inner
+        -- by deconstructing ℓ.  When `t = .univ`, we have ℓ = ℓ_inner.succ,
+        -- so ℓ_inner is the predecessor.
+        match ℓ with
+        | .succ ℓ_inner => do
+            let ℓ_innerE ← reflectULevel ℓ_inner
+            return mkApp (mkConst ``CType.univ) ℓ_innerE
+        | .zero =>
+            -- Unreachable: `.univ : CType (ℓ.succ)` so ℓ ≠ .zero.
+            -- Discharge by emitting a dummy that will never trigger
+            -- — but to keep totality, we still produce an Expr.
+            -- This branch is genuinely dead by typing.
+            return mkApp (mkConst ``CType.univ) (mkConst ``ULevel.zero)
+    | @CType.pi ℓ_a ℓ_b var A B => do
+        let ℓ_aE ← reflectULevel ℓ_a
+        let ℓ_bE ← reflectULevel ℓ_b
+        let varE := mkStrLit var
+        let AE ← reflectCType A
+        let BE ← reflectCType B
+        return mkAppN (mkConst ``CType.pi) #[ℓ_aE, ℓ_bE, varE, AE, BE]
+    | @CType.sigma ℓ_a ℓ_b var A B => do
+        let ℓ_aE ← reflectULevel ℓ_a
+        let ℓ_bE ← reflectULevel ℓ_b
+        let varE := mkStrLit var
+        let AE ← reflectCType A
+        let BE ← reflectCType B
+        return mkAppN (mkConst ``CType.sigma) #[ℓ_aE, ℓ_bE, varE, AE, BE]
+    | .path A a b => do
+        let ℓE ← reflectULevel ℓ
+        let AE ← reflectCType A
+        let aE ← reflectCTerm a
+        let bE ← reflectCTerm b
+        return mkAppN (mkConst ``CType.path) #[ℓE, AE, aE, bE]
+    | .glue φ T f fInv sec ret coh A => do
+        let ℓE ← reflectULevel ℓ
+        let φE ← reflectFaceFormula φ
+        let TE ← reflectCType T
+        let fE ← reflectCTerm f
+        let fInvE ← reflectCTerm fInv
+        let secE ← reflectCTerm sec
+        let retE ← reflectCTerm ret
+        let cohE ← reflectCTerm coh
+        let AE ← reflectCType A
+        return mkAppN (mkConst ``CType.glue)
+          #[ℓE, φE, TE, fE, fInvE, secE, retE, cohE, AE]
+    | .ind S params => do
+        let ℓE ← reflectULevel ℓ
+        let SE ← reflectCTypeSchema S
+        let paramsE ← reflectCTypeAnyList params
+        return mkAppN (mkConst ``CType.ind) #[ℓE, SE, paramsE]
+    | .interval =>
+        return mkConst ``CType.interval
+    | .lift A => do
+        -- `.lift A : CType (ℓ_inner.succ)`.  Same predecessor-extraction
+        -- as `.univ`: `ℓ = ℓ_inner.succ`, so ℓ_inner is `ℓ.pred`.  We
+        -- recurse on A directly (Lean infers the inner level).
+        match ℓ with
+        | .succ ℓ_inner => do
+            let ℓ_innerE ← reflectULevel ℓ_inner
+            let AE ← reflectCType A
+            return mkAppN (mkConst ``CType.lift) #[ℓ_innerE, AE]
+        | .zero =>
+            -- Unreachable: `.lift A : CType (ℓ_inner.succ)`.
+            let AE ← reflectCType A
+            return mkAppN (mkConst ``CType.lift) #[mkConst ``ULevel.zero, AE]
+    | .El P => do
+        let ℓE ← reflectULevel ℓ
+        let PE ← reflectCTerm P
+        return mkAppN (mkConst ``CType.El) #[ℓE, PE]
+
+  /-- Reflect a `CTerm` to a `Lean.Expr`. -/
+  partial def reflectCTerm : CTerm → MetaM Expr
+    | .var x => return mkApp (mkConst ``CTerm.var) (mkStrLit x)
+    | .lam x t => do
+        let te ← reflectCTerm t
+        return mkAppN (mkConst ``CTerm.lam) #[mkStrLit x, te]
+    | .app f a => do
+        let fe ← reflectCTerm f
+        let ae ← reflectCTerm a
+        return mkAppN (mkConst ``CTerm.app) #[fe, ae]
+    | .plam i t => do
+        let ie ← reflectDimVar i
+        let te ← reflectCTerm t
+        return mkAppN (mkConst ``CTerm.plam) #[ie, te]
+    | .papp t r => do
+        let te ← reflectCTerm t
+        let re ← reflectDimExpr r
+        return mkAppN (mkConst ``CTerm.papp) #[te, re]
+    | @CTerm.transp i ℓ A φ t => do
+        let ie ← reflectDimVar i
+        let ℓE ← reflectULevel ℓ
+        let AE ← reflectCType A
+        let φE ← reflectFaceFormula φ
+        let te ← reflectCTerm t
+        return mkAppN (mkConst ``CTerm.transp) #[ie, ℓE, AE, φE, te]
+    | @CTerm.comp i ℓ A φ u t => do
+        let ie ← reflectDimVar i
+        let ℓE ← reflectULevel ℓ
+        let AE ← reflectCType A
+        let φE ← reflectFaceFormula φ
+        let ue ← reflectCTerm u
+        let te ← reflectCTerm t
+        return mkAppN (mkConst ``CTerm.comp) #[ie, ℓE, AE, φE, ue, te]
+    | @CTerm.compN i ℓ A clauses t => do
+        let ie ← reflectDimVar i
+        let ℓE ← reflectULevel ℓ
+        let AE ← reflectCType A
+        let clausesE ← reflectClausesList clauses
+        let te ← reflectCTerm t
+        return mkAppN (mkConst ``CTerm.compN) #[ie, ℓE, AE, clausesE, te]
+    | .glueIn φ t a => do
+        let φE ← reflectFaceFormula φ
+        let te ← reflectCTerm t
+        let ae ← reflectCTerm a
+        return mkAppN (mkConst ``CTerm.glueIn) #[φE, te, ae]
+    | .unglue φ f g => do
+        let φE ← reflectFaceFormula φ
+        let fe ← reflectCTerm f
+        let ge ← reflectCTerm g
+        return mkAppN (mkConst ``CTerm.unglue) #[φE, fe, ge]
+    | .pair a b => do
+        let ae ← reflectCTerm a
+        let be ← reflectCTerm b
+        return mkAppN (mkConst ``CTerm.pair) #[ae, be]
+    | .fst t => do
+        let te ← reflectCTerm t
+        return mkApp (mkConst ``CTerm.fst) te
+    | .snd t => do
+        let te ← reflectCTerm t
+        return mkApp (mkConst ``CTerm.snd) te
+    | .dimExpr r => do
+        let re ← reflectDimExpr r
+        return mkApp (mkConst ``CTerm.dimExpr) re
+    | .ctor S c params args => do
+        let SE ← reflectCTypeSchema S
+        let cE := mkStrLit c
+        let paramsE ← reflectCTypeAnyList params
+        let argsE ← reflectCTermList args
+        return mkAppN (mkConst ``CTerm.ctor) #[SE, cE, paramsE, argsE]
+    | .indElim S params motive branches target => do
+        let SE ← reflectCTypeSchema S
+        let paramsE ← reflectCTypeAnyList params
+        let motiveE ← reflectCTerm motive
+        let branchesE ← reflectBranchesList branches
+        let targetE ← reflectCTerm target
+        return mkAppN (mkConst ``CTerm.indElim)
+          #[SE, paramsE, motiveE, branchesE, targetE]
+    | @CTerm.code ℓ A => do
+        let ℓE ← reflectULevel ℓ
+        let AE ← reflectCType A
+        return mkAppN (mkConst ``CTerm.code) #[ℓE, AE]
+
+  /-- Reflect a `List (Σ ℓ : ULevel, CType ℓ)`.  The Σ pairs are
+      built via `mkSigmaULevelCType`; the list is `List.cons`-spine. -/
+  partial def reflectCTypeAnyList :
+      List (Σ ℓ : ULevel, CType ℓ) → MetaM Expr
+    | [] =>
+        return mkApp (mkConst ``List.nil [Level.zero]) cTypeSigmaExpr
+    | ⟨ℓ, A⟩ :: rest => do
+        let ℓE ← reflectULevel ℓ
+        let AE ← reflectCType A
+        let pairE := mkSigmaULevelCType ℓE AE
+        let restE ← reflectCTypeAnyList rest
+        return mkAppN (mkConst ``List.cons [Level.zero])
+          #[cTypeSigmaExpr, pairE, restE]
+
+  /-- Reflect a `List CTerm`. -/
+  partial def reflectCTermList : List CTerm → MetaM Expr
+    | [] =>
+        return mkApp (mkConst ``List.nil [Level.zero]) (mkConst ``CTerm)
+    | t :: rest => do
+        let te ← reflectCTerm t
+        let restE ← reflectCTermList rest
+        return mkAppN (mkConst ``List.cons [Level.zero])
+          #[mkConst ``CTerm, te, restE]
+
+  /-- Reflect a `List (FaceFormula × CTerm)` — the partial-element
+      clauses of a multi-clause composition. -/
+  partial def reflectClausesList :
+      List (FaceFormula × CTerm) → MetaM Expr
+    | [] =>
+        let pairTy := mkAppN (mkConst ``Prod [Level.zero, Level.zero])
+          #[mkConst ``FaceFormula, mkConst ``CTerm]
+        return mkApp (mkConst ``List.nil [Level.zero]) pairTy
+    | (φ, t) :: rest => do
+        let φE ← reflectFaceFormula φ
+        let te ← reflectCTerm t
+        let pairE := mkAppN (mkConst ``Prod.mk [Level.zero, Level.zero])
+          #[mkConst ``FaceFormula, mkConst ``CTerm, φE, te]
+        let restE ← reflectClausesList rest
+        let pairTy := mkAppN (mkConst ``Prod [Level.zero, Level.zero])
+          #[mkConst ``FaceFormula, mkConst ``CTerm]
+        return mkAppN (mkConst ``List.cons [Level.zero])
+          #[pairTy, pairE, restE]
+
+  /-- Reflect a `List (String × CTerm)` — the named branches of an
+      `indElim`. -/
+  partial def reflectBranchesList :
+      List (String × CTerm) → MetaM Expr
+    | [] =>
+        let pairTy := mkAppN (mkConst ``Prod [Level.zero, Level.zero])
+          #[mkConst ``String, mkConst ``CTerm]
+        return mkApp (mkConst ``List.nil [Level.zero]) pairTy
+    | (n, b) :: rest => do
+        let bE ← reflectCTerm b
+        let pairE := mkAppN (mkConst ``Prod.mk [Level.zero, Level.zero])
+          #[mkConst ``String, mkConst ``CTerm, mkStrLit n, bE]
+        let restE ← reflectBranchesList rest
+        let pairTy := mkAppN (mkConst ``Prod [Level.zero, Level.zero])
+          #[mkConst ``String, mkConst ``CTerm]
+        return mkAppN (mkConst ``List.cons [Level.zero])
+          #[pairTy, pairE, restE]
+
+  /-- Reflect a `CTypeSchema` (the `mk name numParams ctors` form). -/
+  partial def reflectCTypeSchema : CTypeSchema → MetaM Expr := fun S => do
+    match S with
+    | .mk name nP ctors =>
+        let nameE := mkStrLit name
+        let nPE := mkNatLit nP
+        let ctorsE ← reflectCtorSpecList ctors
+        return mkAppN (mkConst ``CTypeSchema.mk) #[nameE, nPE, ctorsE]
+
+  /-- Reflect a `List CtorSpec`. -/
+  partial def reflectCtorSpecList : List CtorSpec → MetaM Expr
+    | [] =>
+        return mkApp (mkConst ``List.nil [Level.zero]) (mkConst ``CtorSpec)
+    | c :: rest => do
+        let cE ← reflectCtorSpec c
+        let restE ← reflectCtorSpecList rest
+        return mkAppN (mkConst ``List.cons [Level.zero])
+          #[mkConst ``CtorSpec, cE, restE]
+
+  /-- Reflect a `CtorSpec` (the `mk name args boundary` form). -/
+  partial def reflectCtorSpec : CtorSpec → MetaM Expr := fun cs => do
+    match cs with
+    | .mk name args bdy =>
+        let nameE := mkStrLit name
+        let argsE ← reflectCTypeArgList args
+        let bdyE ← reflectClausesList bdy
+        return mkAppN (mkConst ``CtorSpec.mk) #[nameE, argsE, bdyE]
+
+  /-- Reflect a `List CTypeArg`. -/
+  partial def reflectCTypeArgList : List CTypeArg → MetaM Expr
+    | [] =>
+        return mkApp (mkConst ``List.nil [Level.zero]) (mkConst ``CTypeArg)
+    | a :: rest => do
+        let aE ← reflectCTypeArg a
+        let restE ← reflectCTypeArgList rest
+        return mkAppN (mkConst ``List.cons [Level.zero])
+          #[mkConst ``CTypeArg, aE, restE]
+
+  /-- Reflect a `CTypeArg` — every constructor: `.type A`, `.param i`,
+      `.self`, `.dim`. -/
+  partial def reflectCTypeArg : CTypeArg → MetaM Expr
+    | @CTypeArg.type ℓ A => do
+        let ℓE ← reflectULevel ℓ
+        let AE ← reflectCType A
+        return mkAppN (mkConst ``CTypeArg.type) #[ℓE, AE]
+    | .param i =>
+        return mkApp (mkConst ``CTypeArg.param) (mkNatLit i)
+    | .self =>
+        return mkConst ``CTypeArg.self
+    | .dim =>
+        return mkConst ``CTypeArg.dim
+end
+
+-- ── §4.  Reification: Expr → ULevel / CType / CTerm ────────────────────────
+
+/-- Reify a `Lean.Expr` back to a `ULevel`.  Returns `none` if the
+    Expr does not match the shape `@ULevel.zero` or `@ULevel.succ <e>`.
+
+    Pattern: walk down `Expr.app`-chains; at each leaf, check the head
+    constant name against `ULevel.zero` / `ULevel.succ`.  This is the
+    strict structural inverse of `reflectULevel`. -/
+partial def reifyULevel : Expr → MetaM (Option ULevel) := fun e => do
+  -- Reduce metadata wrappers and beta-redexes that may be sitting
+  -- around the literal constructor application.
+  let e ← whnf e
+  match e.getAppFnArgs with
+  | (``ULevel.zero, _) => return some .zero
+  | (``ULevel.succ, args) =>
+      if h : args.size = 1 then
+        match ← reifyULevel (args[0]'(by omega)) with
+        | some n => return some (.succ n)
+        | none   => return none
+      else
+        return none
+  | _ => return none
+
+/-- Reify the literal-Nat encoding produced by `mkNatLit n`.  After
+    `whnf`, an `OfNat.ofNat`-shaped numeral reduces to its raw form
+    via `Expr.nat?`. -/
+partial def reifyNatLit (e : Expr) : MetaM (Option Nat) := do
+  let e ← whnf e
+  match e.nat? with
+  | some n => return some n
+  | none =>
+      -- Also accept the raw literal form `.lit (.natVal n)` directly
+      -- (in case `whnf` has already normalised through `OfNat.ofNat`).
+      match e with
+      | .lit (.natVal n) => return some n
+      | _ => return none
+
+/-- Reify a `mkStrLit s`-encoded expression back to its String. -/
+partial def reifyStrLit (e : Expr) : MetaM (Option String) := do
+  let e ← whnf e
+  match e with
+  | .lit (.strVal s) => return some s
+  | _ => return none
+
+mutual
+  /-- Reify a `Lean.Expr` back to a `DimVar`.  Inverts `reflectDimVar`:
+      a single-field structure carrying `name : String`. -/
+  partial def reifyDimVar : Expr → MetaM (Option DimVar) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``DimVar.mk, args) =>
+        -- single field: the dim variable's name string
+        if h : args.size = 1 then
+          match ← reifyStrLit (args[0]'(by omega)) with
+          | some name => return some ⟨name⟩
+          | none      => return none
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `DimExpr`.  Inverts `reflectDimExpr`:
+      one explicit arm per de-Morgan-algebra constructor. -/
+  partial def reifyDimExpr : Expr → MetaM (Option DimExpr) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``DimExpr.zero, _) => return some .zero
+    | (``DimExpr.one,  _) => return some .one
+    | (``DimExpr.var, args) =>
+        -- one DimVar payload
+        if h : args.size = 1 then
+          match ← reifyDimVar (args[0]'(by omega)) with
+          | some i => return some (.var i)
+          | none   => return none
+        else
+          return none
+    | (``DimExpr.inv, args) =>
+        -- one DimExpr payload
+        if h : args.size = 1 then
+          match ← reifyDimExpr (args[0]'(by omega)) with
+          | some r => return some (.inv r)
+          | none   => return none
+        else
+          return none
+    | (``DimExpr.meet, args) =>
+        -- two DimExpr payloads
+        if h : args.size = 2 then
+          match ← reifyDimExpr (args[0]'(by omega)) with
+          | none   => return none
+          | some r =>
+            match ← reifyDimExpr (args[1]'(by omega)) with
+            | none   => return none
+            | some s => return some (.meet r s)
+        else
+          return none
+    | (``DimExpr.join, args) =>
+        -- two DimExpr payloads
+        if h : args.size = 2 then
+          match ← reifyDimExpr (args[0]'(by omega)) with
+          | none   => return none
+          | some r =>
+            match ← reifyDimExpr (args[1]'(by omega)) with
+            | none   => return none
+            | some s => return some (.join r s)
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `FaceFormula`.  Inverts
+      `reflectFaceFormula`: one explicit arm per constructor. -/
+  partial def reifyFaceFormula : Expr → MetaM (Option FaceFormula) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``FaceFormula.bot, _) => return some .bot
+    | (``FaceFormula.top, _) => return some .top
+    | (``FaceFormula.eq0, args) =>
+        -- one DimVar payload (the dimension variable being constrained)
+        if h : args.size = 1 then
+          match ← reifyDimVar (args[0]'(by omega)) with
+          | some i => return some (.eq0 i)
+          | none   => return none
+        else
+          return none
+    | (``FaceFormula.eq1, args) =>
+        -- one DimVar payload
+        if h : args.size = 1 then
+          match ← reifyDimVar (args[0]'(by omega)) with
+          | some i => return some (.eq1 i)
+          | none   => return none
+        else
+          return none
+    | (``FaceFormula.meet, args) =>
+        -- two FaceFormula payloads
+        if h : args.size = 2 then
+          match ← reifyFaceFormula (args[0]'(by omega)) with
+          | none   => return none
+          | some a =>
+            match ← reifyFaceFormula (args[1]'(by omega)) with
+            | none   => return none
+            | some b => return some (.meet a b)
+        else
+          return none
+    | (``FaceFormula.join, args) =>
+        -- two FaceFormula payloads
+        if h : args.size = 2 then
+          match ← reifyFaceFormula (args[0]'(by omega)) with
+          | none   => return none
+          | some a =>
+            match ← reifyFaceFormula (args[1]'(by omega)) with
+            | none   => return none
+            | some b => return some (.join a b)
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `Σ ℓ : ULevel, CType ℓ`.  Inverts
+      `reflectCType` arm-for-arm: nine constructors plus a final
+      catch-all for unrecognised shapes. -/
+  partial def reifyCType :
+      Expr → MetaM (Option (Σ ℓ : ULevel, CType ℓ)) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``CType.univ, args) =>
+        -- args = [ℓ_innerE]; result level = .succ ℓ_inner
+        if h : args.size = 1 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none         => return none
+          | some ℓ_inner => return some ⟨ULevel.succ ℓ_inner, .univ⟩
+        else
+          return none
+    | (``CType.pi, args) =>
+        -- args = [ℓ_aE, ℓ_bE, varE, AE, BE]; result level = max ℓ_a ℓ_b
+        if h : args.size = 5 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none      => return none
+          | some ℓ_a  =>
+            match ← reifyULevel (args[1]'(by omega)) with
+            | none      => return none
+            | some ℓ_b  =>
+              match ← reifyStrLit (args[2]'(by omega)) with
+              | none      => return none
+              | some var  =>
+                match ← reifyCType (args[3]'(by omega)) with
+                | none                     => return none
+                | some ⟨ℓ_a_rec, A⟩ =>
+                  if hA : ℓ_a_rec = ℓ_a then
+                    match ← reifyCType (args[4]'(by omega)) with
+                    | none                   => return none
+                    | some ⟨ℓ_b_rec, B⟩ =>
+                      if hB : ℓ_b_rec = ℓ_b then
+                        let A' : CType ℓ_a := hA ▸ A
+                        let B' : CType ℓ_b := hB ▸ B
+                        return some ⟨ULevel.max ℓ_a ℓ_b, .pi var A' B'⟩
+                      else
+                        return none
+                  else
+                    return none
+        else
+          return none
+    | (``CType.sigma, args) =>
+        -- args = [ℓ_aE, ℓ_bE, varE, AE, BE]; same shape as pi
+        if h : args.size = 5 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none      => return none
+          | some ℓ_a  =>
+            match ← reifyULevel (args[1]'(by omega)) with
+            | none      => return none
+            | some ℓ_b  =>
+              match ← reifyStrLit (args[2]'(by omega)) with
+              | none      => return none
+              | some var  =>
+                match ← reifyCType (args[3]'(by omega)) with
+                | none                     => return none
+                | some ⟨ℓ_a_rec, A⟩ =>
+                  if hA : ℓ_a_rec = ℓ_a then
+                    match ← reifyCType (args[4]'(by omega)) with
+                    | none                   => return none
+                    | some ⟨ℓ_b_rec, B⟩ =>
+                      if hB : ℓ_b_rec = ℓ_b then
+                        let A' : CType ℓ_a := hA ▸ A
+                        let B' : CType ℓ_b := hB ▸ B
+                        return some ⟨ULevel.max ℓ_a ℓ_b, .sigma var A' B'⟩
+                      else
+                        return none
+                  else
+                    return none
+        else
+          return none
+    | (``CType.path, args) =>
+        -- args = [ℓE, AE, aE, bE]; result level = ℓ
+        if h : args.size = 4 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none   => return none
+          | some ℓ =>
+            match ← reifyCType (args[1]'(by omega)) with
+            | none                 => return none
+            | some ⟨ℓ_rec, A⟩ =>
+              if hA : ℓ_rec = ℓ then
+                match ← reifyCTerm (args[2]'(by omega)) with
+                | none   => return none
+                | some a =>
+                  match ← reifyCTerm (args[3]'(by omega)) with
+                  | none   => return none
+                  | some b =>
+                    let A' : CType ℓ := hA ▸ A
+                    return some ⟨ℓ, .path A' a b⟩
+              else
+                return none
+        else
+          return none
+    | (``CType.glue, args) =>
+        -- args = [ℓE, φE, TE, fE, fInvE, secE, retE, cohE, AE]; level = ℓ
+        if h : args.size = 9 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none   => return none
+          | some ℓ =>
+            match ← reifyFaceFormula (args[1]'(by omega)) with
+            | none   => return none
+            | some φ =>
+              match ← reifyCType (args[2]'(by omega)) with
+              | none                 => return none
+              | some ⟨ℓ_T_rec, T⟩ =>
+                if hT : ℓ_T_rec = ℓ then
+                  match ← reifyCTerm (args[3]'(by omega)) with
+                  | none   => return none
+                  | some f =>
+                    match ← reifyCTerm (args[4]'(by omega)) with
+                    | none      => return none
+                    | some fInv =>
+                      match ← reifyCTerm (args[5]'(by omega)) with
+                      | none     => return none
+                      | some sec =>
+                        match ← reifyCTerm (args[6]'(by omega)) with
+                        | none     => return none
+                        | some ret =>
+                          match ← reifyCTerm (args[7]'(by omega)) with
+                          | none     => return none
+                          | some coh =>
+                            match ← reifyCType (args[8]'(by omega)) with
+                            | none                 => return none
+                            | some ⟨ℓ_A_rec, A⟩ =>
+                              if hA : ℓ_A_rec = ℓ then
+                                let T' : CType ℓ := hT ▸ T
+                                let A' : CType ℓ := hA ▸ A
+                                return some ⟨ℓ, .glue φ T' f fInv sec ret coh A'⟩
+                              else
+                                return none
+                else
+                  return none
+        else
+          return none
+    | (``CType.ind, args) =>
+        -- args = [ℓE, SE, paramsE]; result level = ℓ (user-specified)
+        if h : args.size = 3 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none   => return none
+          | some ℓ =>
+            match ← reifyCTypeSchema (args[1]'(by omega)) with
+            | none   => return none
+            | some S =>
+              match ← reifyCTypeAnyList (args[2]'(by omega)) with
+              | none        => return none
+              | some params => return some ⟨ℓ, .ind (ℓ := ℓ) S params⟩
+        else
+          return none
+    | (``CType.interval, _) =>
+        -- nullary; result level = .zero
+        return some ⟨ULevel.zero, .interval⟩
+    | (``CType.lift, args) =>
+        -- args = [ℓ_innerE, AE]; result level = .succ ℓ_inner
+        if h : args.size = 2 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none         => return none
+          | some ℓ_inner =>
+            match ← reifyCType (args[1]'(by omega)) with
+            | none               => return none
+            | some ⟨ℓ_rec, A⟩ =>
+              if hA : ℓ_rec = ℓ_inner then
+                let A' : CType ℓ_inner := hA ▸ A
+                return some ⟨ULevel.succ ℓ_inner, .lift A'⟩
+              else
+                return none
+        else
+          return none
+    | (``CType.El, args) =>
+        -- args = [ℓE, PE]; result level = ℓ
+        if h : args.size = 2 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none   => return none
+          | some ℓ =>
+            match ← reifyCTerm (args[1]'(by omega)) with
+            | none   => return none
+            | some P => return some ⟨ℓ, .El (ℓ := ℓ) P⟩
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `CTerm`.  Inverts `reflectCTerm`
+      arm-for-arm: seventeen constructors plus a final catch-all. -/
+  partial def reifyCTerm : Expr → MetaM (Option CTerm) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``CTerm.var, args) =>
+        -- args = [mkStrLit x]
+        if h : args.size = 1 then
+          match ← reifyStrLit (args[0]'(by omega)) with
+          | some x => return some (.var x)
+          | none   => return none
+        else
+          return none
+    | (``CTerm.lam, args) =>
+        -- args = [mkStrLit x, te]
+        if h : args.size = 2 then
+          match ← reifyStrLit (args[0]'(by omega)) with
+          | none   => return none
+          | some x =>
+            match ← reifyCTerm (args[1]'(by omega)) with
+            | none   => return none
+            | some t => return some (.lam x t)
+        else
+          return none
+    | (``CTerm.app, args) =>
+        -- args = [fe, ae]
+        if h : args.size = 2 then
+          match ← reifyCTerm (args[0]'(by omega)) with
+          | none   => return none
+          | some f =>
+            match ← reifyCTerm (args[1]'(by omega)) with
+            | none   => return none
+            | some a => return some (.app f a)
+        else
+          return none
+    | (``CTerm.plam, args) =>
+        -- args = [ie, te]
+        if h : args.size = 2 then
+          match ← reifyDimVar (args[0]'(by omega)) with
+          | none   => return none
+          | some i =>
+            match ← reifyCTerm (args[1]'(by omega)) with
+            | none   => return none
+            | some t => return some (.plam i t)
+        else
+          return none
+    | (``CTerm.papp, args) =>
+        -- args = [te, re]
+        if h : args.size = 2 then
+          match ← reifyCTerm (args[0]'(by omega)) with
+          | none   => return none
+          | some t =>
+            match ← reifyDimExpr (args[1]'(by omega)) with
+            | none   => return none
+            | some r => return some (.papp t r)
+        else
+          return none
+    | (``CTerm.transp, args) =>
+        -- args = [ie, ℓE, AE, φE, te]
+        if h : args.size = 5 then
+          match ← reifyDimVar (args[0]'(by omega)) with
+          | none   => return none
+          | some i =>
+            match ← reifyULevel (args[1]'(by omega)) with
+            | none   => return none
+            | some ℓ =>
+              match ← reifyCType (args[2]'(by omega)) with
+              | none                 => return none
+              | some ⟨ℓ_rec, A⟩ =>
+                if hA : ℓ_rec = ℓ then
+                  match ← reifyFaceFormula (args[3]'(by omega)) with
+                  | none   => return none
+                  | some φ =>
+                    match ← reifyCTerm (args[4]'(by omega)) with
+                    | none   => return none
+                    | some t =>
+                      let A' : CType ℓ := hA ▸ A
+                      return some (.transp i (ℓ := ℓ) A' φ t)
+                else
+                  return none
+        else
+          return none
+    | (``CTerm.comp, args) =>
+        -- args = [ie, ℓE, AE, φE, ue, te]
+        if h : args.size = 6 then
+          match ← reifyDimVar (args[0]'(by omega)) with
+          | none   => return none
+          | some i =>
+            match ← reifyULevel (args[1]'(by omega)) with
+            | none   => return none
+            | some ℓ =>
+              match ← reifyCType (args[2]'(by omega)) with
+              | none                 => return none
+              | some ⟨ℓ_rec, A⟩ =>
+                if hA : ℓ_rec = ℓ then
+                  match ← reifyFaceFormula (args[3]'(by omega)) with
+                  | none   => return none
+                  | some φ =>
+                    match ← reifyCTerm (args[4]'(by omega)) with
+                    | none   => return none
+                    | some u =>
+                      match ← reifyCTerm (args[5]'(by omega)) with
+                      | none   => return none
+                      | some t =>
+                        let A' : CType ℓ := hA ▸ A
+                        return some (.comp i (ℓ := ℓ) A' φ u t)
+                else
+                  return none
+        else
+          return none
+    | (``CTerm.compN, args) =>
+        -- args = [ie, ℓE, AE, clausesE, te]
+        if h : args.size = 5 then
+          match ← reifyDimVar (args[0]'(by omega)) with
+          | none   => return none
+          | some i =>
+            match ← reifyULevel (args[1]'(by omega)) with
+            | none   => return none
+            | some ℓ =>
+              match ← reifyCType (args[2]'(by omega)) with
+              | none                 => return none
+              | some ⟨ℓ_rec, A⟩ =>
+                if hA : ℓ_rec = ℓ then
+                  match ← reifyClausesList (args[3]'(by omega)) with
+                  | none         => return none
+                  | some clauses =>
+                    match ← reifyCTerm (args[4]'(by omega)) with
+                    | none   => return none
+                    | some t =>
+                      let A' : CType ℓ := hA ▸ A
+                      return some (.compN i (ℓ := ℓ) A' clauses t)
+                else
+                  return none
+        else
+          return none
+    | (``CTerm.glueIn, args) =>
+        -- args = [φE, te, ae]
+        if h : args.size = 3 then
+          match ← reifyFaceFormula (args[0]'(by omega)) with
+          | none   => return none
+          | some φ =>
+            match ← reifyCTerm (args[1]'(by omega)) with
+            | none   => return none
+            | some t =>
+              match ← reifyCTerm (args[2]'(by omega)) with
+              | none   => return none
+              | some a => return some (.glueIn φ t a)
+        else
+          return none
+    | (``CTerm.unglue, args) =>
+        -- args = [φE, fe, ge]
+        if h : args.size = 3 then
+          match ← reifyFaceFormula (args[0]'(by omega)) with
+          | none   => return none
+          | some φ =>
+            match ← reifyCTerm (args[1]'(by omega)) with
+            | none   => return none
+            | some f =>
+              match ← reifyCTerm (args[2]'(by omega)) with
+              | none   => return none
+              | some g => return some (.unglue φ f g)
+        else
+          return none
+    | (``CTerm.pair, args) =>
+        -- args = [ae, be]
+        if h : args.size = 2 then
+          match ← reifyCTerm (args[0]'(by omega)) with
+          | none   => return none
+          | some a =>
+            match ← reifyCTerm (args[1]'(by omega)) with
+            | none   => return none
+            | some b => return some (.pair a b)
+        else
+          return none
+    | (``CTerm.fst, args) =>
+        -- args = [te]
+        if h : args.size = 1 then
+          match ← reifyCTerm (args[0]'(by omega)) with
+          | none   => return none
+          | some t => return some (.fst t)
+        else
+          return none
+    | (``CTerm.snd, args) =>
+        -- args = [te]
+        if h : args.size = 1 then
+          match ← reifyCTerm (args[0]'(by omega)) with
+          | none   => return none
+          | some t => return some (.snd t)
+        else
+          return none
+    | (``CTerm.dimExpr, args) =>
+        -- args = [re]
+        if h : args.size = 1 then
+          match ← reifyDimExpr (args[0]'(by omega)) with
+          | none   => return none
+          | some r => return some (.dimExpr r)
+        else
+          return none
+    | (``CTerm.ctor, args) =>
+        -- args = [SE, cE, paramsE, argsE]
+        if h : args.size = 4 then
+          match ← reifyCTypeSchema (args[0]'(by omega)) with
+          | none   => return none
+          | some S =>
+            match ← reifyStrLit (args[1]'(by omega)) with
+            | none   => return none
+            | some c =>
+              match ← reifyCTypeAnyList (args[2]'(by omega)) with
+              | none        => return none
+              | some params =>
+                match ← reifyCTermList (args[3]'(by omega)) with
+                | none      => return none
+                | some args' => return some (.ctor S c params args')
+        else
+          return none
+    | (``CTerm.indElim, args) =>
+        -- args = [SE, paramsE, motiveE, branchesE, targetE]
+        if h : args.size = 5 then
+          match ← reifyCTypeSchema (args[0]'(by omega)) with
+          | none   => return none
+          | some S =>
+            match ← reifyCTypeAnyList (args[1]'(by omega)) with
+            | none        => return none
+            | some params =>
+              match ← reifyCTerm (args[2]'(by omega)) with
+              | none        => return none
+              | some motive =>
+                match ← reifyBranchesList (args[3]'(by omega)) with
+                | none          => return none
+                | some branches =>
+                  match ← reifyCTerm (args[4]'(by omega)) with
+                  | none        => return none
+                  | some target =>
+                    return some (.indElim S params motive branches target)
+        else
+          return none
+    | (``CTerm.code, args) =>
+        -- args = [ℓE, AE]
+        if h : args.size = 2 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none   => return none
+          | some ℓ =>
+            match ← reifyCType (args[1]'(by omega)) with
+            | none                 => return none
+            | some ⟨ℓ_rec, A⟩ =>
+              if hA : ℓ_rec = ℓ then
+                let A' : CType ℓ := hA ▸ A
+                return some (.code (ℓ := ℓ) A')
+              else
+                return none
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `List (Σ ℓ : ULevel, CType ℓ)`.
+      Inverts `reflectCTypeAnyList`: List.nil/cons spine over Sigma pairs. -/
+  partial def reifyCTypeAnyList :
+      Expr → MetaM (Option (List (Σ ℓ : ULevel, CType ℓ))) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``List.nil, _) =>
+        -- empty list; element-type arg ignored (encoded by reflect side)
+        return some []
+    | (``List.cons, args) =>
+        -- args = [elemTy, headPair, tail]
+        if h : args.size = 3 then
+          -- head is `Sigma.mk _ _ ℓE AE`; decode it directly
+          let headE ← whnf (args[1]'(by omega))
+          match headE.getAppFnArgs with
+          | (``Sigma.mk, sargs) =>
+              -- sargs = [ULevel, family, ℓE, AE]
+              if hs : sargs.size = 4 then
+                match ← reifyULevel (sargs[2]'(by omega)) with
+                | none   => return none
+                | some ℓ =>
+                  match ← reifyCType (sargs[3]'(by omega)) with
+                  | none                 => return none
+                  | some ⟨ℓ_rec, A⟩ =>
+                    if hA : ℓ_rec = ℓ then
+                      let A' : CType ℓ := hA ▸ A
+                      match ← reifyCTypeAnyList (args[2]'(by omega)) with
+                      | none      => return none
+                      | some rest => return some (⟨ℓ, A'⟩ :: rest)
+                    else
+                      return none
+              else
+                return none
+          | _ => return none
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `List CTerm`.  Inverts
+      `reflectCTermList`: List.nil/cons spine over CTerm elements. -/
+  partial def reifyCTermList :
+      Expr → MetaM (Option (List CTerm)) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``List.nil, _) =>
+        -- empty list
+        return some []
+    | (``List.cons, args) =>
+        -- args = [elemTy, headTerm, tail]
+        if h : args.size = 3 then
+          match ← reifyCTerm (args[1]'(by omega)) with
+          | none   => return none
+          | some t =>
+            match ← reifyCTermList (args[2]'(by omega)) with
+            | none      => return none
+            | some rest => return some (t :: rest)
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `List (FaceFormula × CTerm)`.
+      Inverts `reflectClausesList`: List.nil/cons spine over Prod pairs. -/
+  partial def reifyClausesList :
+      Expr → MetaM (Option (List (FaceFormula × CTerm))) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``List.nil, _) =>
+        -- empty clause list
+        return some []
+    | (``List.cons, args) =>
+        -- args = [elemTy, headPair, tail]
+        if h : args.size = 3 then
+          let headE ← whnf (args[1]'(by omega))
+          match headE.getAppFnArgs with
+          | (``Prod.mk, pargs) =>
+              -- pargs = [αTy, βTy, φE, tE]
+              if hp : pargs.size = 4 then
+                match ← reifyFaceFormula (pargs[2]'(by omega)) with
+                | none   => return none
+                | some φ =>
+                  match ← reifyCTerm (pargs[3]'(by omega)) with
+                  | none   => return none
+                  | some t =>
+                    match ← reifyClausesList (args[2]'(by omega)) with
+                    | none      => return none
+                    | some rest => return some ((φ, t) :: rest)
+              else
+                return none
+          | _ => return none
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `List (String × CTerm)`.  Inverts
+      `reflectBranchesList`: List.nil/cons spine over Prod pairs. -/
+  partial def reifyBranchesList :
+      Expr → MetaM (Option (List (String × CTerm))) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``List.nil, _) =>
+        -- empty branch list
+        return some []
+    | (``List.cons, args) =>
+        -- args = [elemTy, headPair, tail]
+        if h : args.size = 3 then
+          let headE ← whnf (args[1]'(by omega))
+          match headE.getAppFnArgs with
+          | (``Prod.mk, pargs) =>
+              -- pargs = [αTy, βTy, nameE, bodyE]
+              if hp : pargs.size = 4 then
+                match ← reifyStrLit (pargs[2]'(by omega)) with
+                | none   => return none
+                | some n =>
+                  match ← reifyCTerm (pargs[3]'(by omega)) with
+                  | none   => return none
+                  | some b =>
+                    match ← reifyBranchesList (args[2]'(by omega)) with
+                    | none      => return none
+                    | some rest => return some ((n, b) :: rest)
+              else
+                return none
+          | _ => return none
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `CTypeSchema`.  Inverts
+      `reflectCTypeSchema`: the `mk name numParams ctors` form. -/
+  partial def reifyCTypeSchema : Expr → MetaM (Option CTypeSchema) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``CTypeSchema.mk, args) =>
+        -- args = [nameE, nPE, ctorsE]
+        if h : args.size = 3 then
+          match ← reifyStrLit (args[0]'(by omega)) with
+          | none      => return none
+          | some name =>
+            match ← reifyNatLit (args[1]'(by omega)) with
+            | none    => return none
+            | some nP =>
+              match ← reifyCtorSpecList (args[2]'(by omega)) with
+              | none       => return none
+              | some ctors => return some (.mk name nP ctors)
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `List CtorSpec`.  Inverts
+      `reflectCtorSpecList`: List.nil/cons spine over CtorSpecs. -/
+  partial def reifyCtorSpecList :
+      Expr → MetaM (Option (List CtorSpec)) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``List.nil, _) =>
+        -- empty CtorSpec list
+        return some []
+    | (``List.cons, args) =>
+        -- args = [elemTy, head, tail]
+        if h : args.size = 3 then
+          match ← reifyCtorSpec (args[1]'(by omega)) with
+          | none   => return none
+          | some c =>
+            match ← reifyCtorSpecList (args[2]'(by omega)) with
+            | none      => return none
+            | some rest => return some (c :: rest)
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `CtorSpec`.  Inverts
+      `reflectCtorSpec`: the `mk name args boundary` form. -/
+  partial def reifyCtorSpec : Expr → MetaM (Option CtorSpec) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``CtorSpec.mk, args) =>
+        -- args = [nameE, argsE, bdyE]
+        if h : args.size = 3 then
+          match ← reifyStrLit (args[0]'(by omega)) with
+          | none      => return none
+          | some name =>
+            match ← reifyCTypeArgList (args[1]'(by omega)) with
+            | none       => return none
+            | some args' =>
+              match ← reifyClausesList (args[2]'(by omega)) with
+              | none     => return none
+              | some bdy => return some (.mk name args' bdy)
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `List CTypeArg`.  Inverts
+      `reflectCTypeArgList`: List.nil/cons spine over CTypeArgs. -/
+  partial def reifyCTypeArgList :
+      Expr → MetaM (Option (List CTypeArg)) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``List.nil, _) =>
+        -- empty CTypeArg list
+        return some []
+    | (``List.cons, args) =>
+        -- args = [elemTy, head, tail]
+        if h : args.size = 3 then
+          match ← reifyCTypeArg (args[1]'(by omega)) with
+          | none   => return none
+          | some a =>
+            match ← reifyCTypeArgList (args[2]'(by omega)) with
+            | none      => return none
+            | some rest => return some (a :: rest)
+        else
+          return none
+    | _ => return none
+
+  /-- Reify a `Lean.Expr` back to a `CTypeArg`.  Inverts
+      `reflectCTypeArg`: four constructors (.type, .param, .self, .dim). -/
+  partial def reifyCTypeArg : Expr → MetaM (Option CTypeArg) := fun e => do
+    let e ← whnf e
+    match e.getAppFnArgs with
+    | (``CTypeArg.type, args) =>
+        -- args = [ℓE, AE]; needs Sigma-style level coherence check
+        if h : args.size = 2 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none   => return none
+          | some ℓ =>
+            match ← reifyCType (args[1]'(by omega)) with
+            | none                 => return none
+            | some ⟨ℓ_rec, A⟩ =>
+              if hA : ℓ_rec = ℓ then
+                let A' : CType ℓ := hA ▸ A
+                return some (.type (ℓ := ℓ) A')
+              else
+                return none
+        else
+          return none
+    | (``CTypeArg.param, args) =>
+        -- args = [iE]
+        if h : args.size = 1 then
+          match ← reifyNatLit (args[0]'(by omega)) with
+          | none   => return none
+          | some i => return some (.param i)
+        else
+          return none
+    | (``CTypeArg.self, _) => return some .self
+    | (``CTypeArg.dim,  _) => return some .dim
+    | _ => return none
+end
+
+-- ── §5.  Contract registry ──────────────────────────────────────────────────
+
+/-- Type-erased Contract package — bundles a Contract with its
+    universe level so the registry can hold heterogeneous-level
+    entries homogeneously. -/
+structure ContractEntry where
+  /-- The universe level the contract operates at. -/
+  level    : ULevel
+  /-- The contract itself: a function from CType ℓ to CTerm. -/
+  contract : Contract level
+
+/-- The contract registry: maps `Lean.Name` to `ContractEntry`.
+
+    Initialised empty.  Contracts register themselves in their
+    defining module's `initialize` block via `Contract.register`;
+    tactics and other consumers look them up by name. -/
+initialize contractRegistry : IO.Ref (Std.HashMap Lean.Name ContractEntry) ←
+  IO.mkRef ∅
+
+/-- Register a Contract under the given `Lean.Name`.  Subsequent
+    lookups via `Contract.lookupByName n` return the newly registered
+    entry.  Re-registering the same name overwrites the previous
+    entry (last-write-wins). -/
+def Contract.register (n : Lean.Name) (e : ContractEntry) : IO Unit := do
+  contractRegistry.modify (·.insert n e)
+
+/-- Look up a Contract by name.  Returns `none` if no entry has been
+    registered under `n`. -/
+def Contract.lookupByName (n : Lean.Name) : IO (Option ContractEntry) := do
+  let registry ← contractRegistry.get
+  return registry[n]?
+
+/-- List all registered Contract names (in arbitrary HashMap order). -/
+def Contract.allRegistered : IO (List Lean.Name) := do
+  let registry ← contractRegistry.get
+  return registry.toList.map (·.1)
+
+-- ── §6.  Round-trip theorems ────────────────────────────────────────────────
+
+/-- Round-trip property: reflecting then reifying a CTerm in a single
+    `MetaM` computation yields `pure (some t)`.
+
+    Stated as an equation between two `MetaM (Option CTerm)`
+    computations: the `reflectCTerm` followed by `reifyCTerm` chain
+    must produce the original CTerm wrapped in `some`.
+
+    Proof outline (structural induction on `t`):
+      · Each CTerm constructor's reflect-arm produces an Expr whose
+        `getAppFnArgs` yields the constructor's name and reflected
+        sub-payloads.
+      · Each CTerm constructor's reify-arm (once written, currently
+        sorry'd above) inverts the reflect-arm exactly: reading off
+        `getAppFnArgs` recovers the constructor's name; recursive
+        `reifyCType` / `reifyCTerm` / `reifyDimVar` / `reifyDimExpr` /
+        `reifyFaceFormula` calls invert the sub-payload reflections
+        by induction.
+      · The literal-encoding round-trips (`mkStrLit s` ↔ extract
+        `Expr.litValue? = some (.strVal s)`; `mkNatLit n` ↔ extract
+        `Expr.natLitValue?`) close at the leaves.
+
+    The proof is currently sorry'd pending the meta-level
+    `Expr`-equality framework that gives reduction-up-to-elaboration
+    semantics for `MetaM`-bound equations. -/
+theorem reflectCTerm_reifyCTerm_roundtrip (t : CTerm) :
+    (do let e ← reflectCTerm t; reifyCTerm e) = (pure (some t) : MetaM (Option CTerm)) := by
+  -- waits on: meta-level reflection-roundtrip framework
+  --           (Expr-equality up to elaboration in a fixed Environment).
+  --           Once the framework lands, this discharges by structural
+  --           induction on `t`, with each constructor's case closed by
+  --           `simp [reflectCTerm, reifyCTerm, mkApp, mkAppN, ...]` and
+  --           the corresponding arm of the (yet-to-be-completed)
+  --           reifyCTerm body.
+  sorry
+
+/-- Round-trip property: reflecting then reifying a CType in a single
+    `MetaM` computation yields `pure (some ⟨ℓ, T⟩)`.  Same shape and
+    proof outline as the CTerm round-trip. -/
+theorem reflectCType_reifyCType_roundtrip
+    {ℓ : ULevel} (T : CType ℓ) :
+    (do let e ← reflectCType T; reifyCType e) =
+      (pure (some ⟨ℓ, T⟩) : MetaM (Option (Σ ℓ : ULevel, CType ℓ))) := by
+  -- waits on: meta-level reflection-roundtrip framework, as above.
+  sorry
+
+/-- Round-trip property: reflecting then reifying a `ULevel` in a
+    single `MetaM` computation yields `pure (some ℓ)`.  This is the
+    only round-trip whose proof obligation is fully elaborable
+    structurally — it does not depend on the larger `Expr`-elaboration
+    framework.  Stated here for symmetry with the CType / CTerm
+    round-trips. -/
+theorem reflectULevel_reifyULevel_roundtrip (ℓ : ULevel) :
+    (do let e ← reflectULevel ℓ; reifyULevel e) =
+      (pure (some ℓ) : MetaM (Option ULevel)) := by
+  -- waits on: meta-level reflection-roundtrip framework
+  --           (Expr-equality up to elaboration in a fixed Environment),
+  --           even though the structural recursion on `ℓ` is two-arm
+  --           and small, the `whnf` step in `reifyULevel` operates in
+  --           the elaborator monad and its image equation requires the
+  --           same framework as the CType / CTerm round-trips.
+  sorry
+
+/-- Reflection preserves the CType-typing relationship: if the CTerm
+    `t` has CType `T` in the empty context (according to the engine's
+    `HasType` judgment), then there exist Lean Exprs `et` and `eT`
+    that are the reflections of `t` and `T` respectively, and they
+    stand in a corresponding meta-level typing relationship under
+    elaboration (i.e., `et : eT` once the Exprs are elaborated in a
+    context with the engine's namespace open).
+
+    The Lean-side typing-correspondence statement is:
+
+        HasType [] t T  →
+        ∃ (eT et : Expr),
+          (do let e1 ← reflectCType T
+              let e2 ← reflectCTerm t
+              pure (e1, e2)) = (pure (eT, et) : MetaM (Expr × Expr))
+
+    The substantive content (that `et : eT` after elaboration) lives
+    in the `MetaM`-equation: the reflected pair, evaluated in the
+    elaborator, must agree with the original `(T, t)` pair under the
+    encoding.
+
+    Proof depends on the same meta-level `Expr`-elaboration framework
+    that the round-trip theorems wait on. -/
+theorem reflect_preserves_typing
+    {ℓ : ULevel} (t : CTerm) (T : CType ℓ)
+    (_h : HasType [] t T) :
+    ∃ (eT et : Expr),
+      (do
+        let e1 ← reflectCType T
+        let e2 ← reflectCTerm t
+        pure (e1, e2)) = (pure (eT, et) : MetaM (Expr × Expr)) := by
+  -- waits on: a meta-level Expr-typing framework that reads the
+  --           elaborated types of `reflectCTerm t` and
+  --           `reflectCType T` and compares them.  The current
+  --           statement asserts only the existence of the reflected
+  --           pair and an equation tying it to the literal pair; the
+  --           full `et : eT` correspondence requires the elaborator
+  --           framework to be available at the meta level.
+  sorry
+
+end CubicalTransport.Reflect