ParamTransfer — the single entry point

import Transfer loads the whole engine: a Lean 4 framework for reasoning up to a registered relation. It draws on modular parametricity (Trocq's graded map-class lattice and combinators), relational transfer and data refinement (CoqEAL), heterogeneous congruence from cubical type theory (the set-level form; Gjørup–Spitters), and congruence-closure algorithms. On top of these it provides one auto tactic that unifies several native Lean relational tactics (congr/gcongr, norm_cast, cast-rw, transfer, conv, aesop/grind) behind a single inference rule. Trocq is the largest single influence. The framework applies to compiler verification and to program verification (mvcgen / Std.Do triples, hax-extracted code). Full overview, file map and usage: README.md.

The five layers (bottom-up; see the README table for the file map)

0. Relation hierarchy — ParamHierarchy (MapClass = map0…map4, Map_k.Has, Param (m n) A B), ParamLevel (lattice ⊑/meet + the arrowReq/forallReq level tables), ParamWeaken (downgrade), ParamEquiv (bridges from the encoding classes).
1. Combinators — ParamArrow (function rule, map0–map4), ParamForall (dependent-Π rule).
2. Synthesis — ParamSynth(Ext) (HasParam: resolution = Elpi search) + ParamResolve (param_resolve, the level-directed search).
3. Transfer — ParamTransfer / ParamForallNested (forallTransfer), ParamTransferTac (param_transfer, auto-resolved domain).
4. Term-level ⟦·⟧ — ParamTranslate (core), ParamDB (@[param] registry), ParamTranslateTy (change-of-rep binders), ParamTranslateOp (operators), ParamTranslateFull (the integrated translator + #transfer).

The boundary (proven)

UnivalenceStatus.univalence_inconsistent : Univalence → False. Type-level univalence is inconsistent in Lean (Eq : … → Prop is proof-irrelevant), so the map4/Type-motive level is unreachable. The univalence-free fragment realized here is therefore the entire consistent space — and, since Lean's funext is free, it is wider than Coq's univalence-free cap.