The integrated term-level translator ⟦·⟧ (capstone)

Combines the three extensions into one parametricity translation:

• var — relatedness hypothesis from the local context;
• const — resolved from the ambient @[param] registry (ParamDB), no explicit database;
• operator spine (a * b = @HMul.hMul … a b) — the operator/arity rule (ParamTranslateOp): strip the leading type/instance args, apply the registered binary witness to the translated value args;
• app — the parametricity application fR a a' aR;
• lam — the type-translation rule (ParamTranslateTy): the binder may change representation (x : A ↦ x' : A') at the relation PA from translateTy, with hypothesis xr : PA x x'.

translateAll is the single function with all rules; #transfer t runs it against the ambient registry. This is the term-level ⟦·⟧ for the first-order fragment (const/var/app/lam/operators, registry-driven, with change-of-representation binders). The remaining case — dependent Π/recursors and the Type-valued motive — is the univalence cap, which UnivalenceStatus.univalence_inconsistent proves is unreachable in Lean by necessity.

partial def Transfer.Param.translateAll (opdb : OpDB) (tdb : Lean.NameMap (Lean.Expr × Lean.Expr)) (ctx : Std.HashMap Lean.FVarId (Lean.Expr × Lean.Expr)) (db : Lean.NameMap (Lean.Expr × Lean.Expr)) : Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)

The integrated translation: operator-spine, registry const, app, the type-translating lam, and var. opdb is the operator database, tdb the type-relation database, db the (registry-materialised) constant database.

Registered witnesses (downstream of ParamDB, so @[param] works here)

theorem Transfer.Param.succWitFull : RArrow Eq Eq Nat.succ Nat.succ

Nat.succ related to itself (diagonal), registered in the @[param] database.

theorem Transfer.Param.mulWitFull : RArrow Eq (RArrow Eq Eq) Nat.mul Nat.mul

Nat.mul related to itself, curried through the function relation (for the operator rule on *).

def Transfer.Param.demoOpDB : OpDB

The demo operator database: HMul.hMul (4 leading type/instance args) ↦ Nat.mul with witness mulWitFull.

Equations

• Transfer.Param.demoOpDB = ∅.insert `HMul.hMul (4, Lean.Expr.const `Nat.mul [], Lean.Expr.const `Transfer.Param.mulWitFull [])

def Transfer.Param.«command#transfer_» : Lean.ParserDescr

#transfer t — the integrated translation against the ambient @[param] registry (constants) + the demo operator database, logging the transferred term and the relatedness proof's type.

Equations

• One or more equations did not get rendered due to their size.

Demonstrations — all rules together, registry-driven

The constant Nat.succ is resolved from the registry, * via the operator rule, under a lam; no explicit database at any call site.