The binder type-translation rule (change-of-representation)

ParamTranslate.lean builds the term-level parametricity translation ⟦·⟧ with the four core rules var/const/app/lam, but its lam rule fixes the binder's domain relation to the diagonal Eq: a bound x : A is transferred to x' : A at the same type, with relatedness hypothesis x = x'. That is the same-representation fragment.

This module lifts that restriction. It adds the type-translation component of ⟦·⟧ — the sort/binder-domain rule — so a binder may change representation: x : A ↦ x' : A' with a relatedness hypothesis xr : PA x x' at a non-Eq relation PA : A → A' → Prop. Concretely it provides:

• translateTy — ⟦·⟧ on a type expr A, returning (A', PA) where A' is the transferred type and PA : A → A' → Prop is the chosen relation:
  • a registered base type name → its (A', PA) from the type database;
  • an arrow A → B → (A' → B', RArrow PA_A PA_B) (recurse on domain and codomain, then assemble both the arrow type and the function relation RArrow as Exprs);
  • any unregistered/other type → the diagonal (A, @Eq A) (same-representation default, so translateFull degenerates to translate on Eq-only inputs).
• translateFull — a copy of translate whose lam rule consults translateTy to pick the binder's domain type and relation. var/const/ app are unchanged.

The type database is the type-level analogue of translate's constant database: a NameMap (Expr × Expr) mapping a base type's name to (A', PA) (the type's Param.R). As there, it is passed explicitly rather than held in a persistent attribute.

Combined with the app/const/var rules, this covers cross-representation transfer: under a change-of-representation binder, a registered constant g : A → B (whose database witness gR : RArrow PA PB g g' relates it to its transferred g') is transported, and the synthesized proof relates g x to g' x' across the *non-Eq* binder relation.

Scope

translateTy's arrow case is first-order: it handles a non-dependent arrow A → B. A dependent Π (x : A), B x — where the binder type B depends on an earlier binder — is not handled (the recursion would have to thread the parametricity context into translateTy); such forall-exprs fall to the Eq default. Type-valued motives (relating types-as-data, the peano_bin_nat case) likewise remain the univalence-capped boundary, exactly as for ParamTranslate. This module adds the change-of-representation binder rule for the first-order fragment.

The type-translation rule ⟦·⟧ on types

partial def Transfer.Param.translateTy (tdb : Lean.NameMap (Lean.Expr × Lean.Expr)) : Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)

⟦·⟧ on a type expr. Given a type database tdb mapping a base type's name to (A', PA) (its Param.R), returns (A', PA) for the input type: A' is the transferred type, PA : A → A' → Prop the chosen relation.

• a registered base type name → its (A', PA) from tdb;
• a non-dependent arrow A → B → (A' → B', RArrow PA_A PA_B), recursing on domain and codomain and assembling the arrow type and the function relation RArrow (see ParamTranslate.RArrow) as Exprs;
• anything else (unregistered base, dependent Π, sorts) → the diagonal (A, @Eq A), i.e. treat as the same representation.

The diagonal default makes translateFull agree with translate on inputs whose binders all sit at Eq.

The full translation with the change-of-representation lam rule

partial def Transfer.Param.translateFull (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 term-level parametricity translation ⟦·⟧ with a type-directed lam rule. Like ParamTranslate.translate (same var/const/app rules), but the lam rule consults translateTy tdb on the binder's type to obtain the transferred domain A' and the binder relation PA : A → A' → Prop, then introduces x : A, x' : A', and xr : PA x x' (the relatedness hypothesis at the chosen relation, not necessarily Eq). This is the change-of- representation binder rule.

Returns (t', tR) with t' the transferred term and tR a proof of relatedness. With tdb = ∅ it reduces to translate (every binder defaults to Eq).

A registered change-of-representation pair

A cross-type relation Nat ~ Int and a constant witness that survives it, used by the demo below. NatIntR n i := (↑n = i) relates a Nat to the Int it injects to; succR witnesses that Nat.succ and (· + 1) send NatIntR-related arguments to NatIntR-related results — i.e. Nat.succ and (· + 1) are related at RArrow NatIntR NatIntR.

def Transfer.Param.NatIntR (n : Nat) (i : Int) : Prop

The relation registering Nat ↦ Int: a Nat is related to the Int it injects to. (Non-Eq — the two sides have different types.)

Equations

• Transfer.Param.NatIntR n i = (↑n = i)

theorem Transfer.Param.succR : RArrow NatIntR NatIntR Nat.succ fun (i : Int) => i + 1

Nat.succ and (· + 1) are related at RArrow NatIntR NatIntR: they send NatIntR-related arguments to NatIntR-related results. This is the database witness for the change-of-representation demo.

Demonstrations

run_meta blocks build the transferred term + relatedness proof; inferType (which errors on an ill-typed term) kernel-checks each, so these are checked validations. The demos exercise, in order: (a) translateTy on an arrow type; (b) translateFull reproducing the Eq-lam regression; (c) translateFull on a binder whose domain changes representation (Nat ↦ Int) with a relatedness hypothesis that is not Eq.