The dependent-Π (∀ / forall) parametricity rule

A Lean port of Trocq's std/Param_forall.v (https://github.com/rocq-community/trocq): the combinators that build a Param annotated relation on a dependent function space (∀ a, B a) from a Param relation PA on the domain and a family PB of Param relations on the codomain, one for each pair of related inputs.

This is the dependent-Π / dependent-motive rule of the parametricity translation. Where the arrow rule (ParamArrow.lean) relates f : A → B and f' : A' → B' with a constant codomain relation, here the codomain type B a (resp. B' a') depends on the argument, and the relation tying f a : B a to f' a' : B' a' is itself indexed by the witness aR : PA.R a a'.

The funext advantage

Coq's std variant gates the map2b/map3 forall combinators on a `{Funext} instance. Lean has funext as a theorem, so those gates are unnecessary. The forward map of the dependent-Π rule — Map1_forall below — is univalence-free: it only needs the domain's backward structure at level map2a (a map plus map a' = a → R a a'), which Param02a/Param04 all provide. This is the axiom-free part: the dependent motive's forward transfer.

Where univalence enters (Map2a_forall)

The forward map Map1_forall instantiates the codomain family at the single related pair (PA.bwd.map a', a') reachable from the backward map applied to a'. That is enough to produce an element of B' a' from f, i.e. to build the map field of Map2aHas. But the next level Map2a_forall also needs the map_in_R field:

map_in_R : ∀ f g, (Map1_forall …).map f = g → R_forall PA PB f g,

i.e. for an arbitrary related pair (a, a') with witness aR : PA.R a a', it must relate (map f) a' : B' a' — which was built using the specific witness PA.bwd.map_in_R a' (PA.bwd.map a') rfl at the input PA.bwd.map a' — to f a : B a at the given a. Reconciling the two requires identifying the input a with PA.bwd.map a' and transporting the codomain family PB along that identification coherently. Over a general Param, the only data that delivers a coherent such transport — bwd.map a' = a reflecting back to R a a' and round-tripping (R_in_mapK) — is the domain backward relation at map4, i.e. a univalent equivalence. Hence Map2a_forall requires PA : Param04 (domain backward map4), and that map4 coherence is where the dependent-Π rule requires univalence: the dependent-Π output at level ≥ map2a needs the domain relation to be an equivalence so the motive transports.

Concretely, the signature not implemented here (would require the map4/univalence machinery; stated as a comment, no sorry):

def Map2a_forall (PA : Param .map0 .map4 A A') (PB : ∀ a a', PA.R a a' → Param .map2a .map0 (B a) (B' a')) : Map2aHas (R_forall PA PB)

with the map field reusing Map1_forall's, and the map_in_R field the part that consumes the map4 coherence (PA.bwd.R_in_mapK) to transport PB.

Accessor dictionary (Coq → Lean), backward direction of PA

Recall PA.bwd : MapHas n (symRel PA.R), and symRel PA.R a' a is defeq PA.R a a'. So at the input levels where the field exists:

• PA.bwd.map : A' → A (PA bwd ≥ map1)
• PA.bwd.map_in_R : ∀ a' a, PA.bwd.map a' = a → PA.R a a' (PA bwd ≥ map2a)
• (PB a a' aR).fwd.map : B a → B' a' (PB fwd ≥ map1)

The dependent forall relation R_forall

def Transfer.Param.R_forall {A A' : Type u} {B : A → Type u} {B' : A' → Type u} {mA nA mB nB : MapClass} (PA : Param mA nA A A') (PB : (a : A) → (a' : A') → PA.R a a' → Param mB nB (B a) (B' a')) : ((a : A) → B a) → ((a' : A') → B' a') → Prop

Trocq R_forall: two dependent functions are related when, for every pair of PA-related inputs a, a' with witness aR, their outputs are (PB a a' aR)-related. The codomain relation is a family indexed by the relatedness witness aR : PA.R a a'. Only the R fields are touched, so the level parameters stay fully polymorphic.

Equations

• Transfer.Param.R_forall PA PB f f' = ∀ (a : A) (a' : A') (aR : PA.R a a'), (PB a a' aR).R (f a) (f' a')

map0 — no structure

def Transfer.Param.Map0_forall {A A' : Type u} {B : A → Type u} {B' : A' → Type u} {mA nA mB nB : MapClass} (PA : Param mA nA A A') (PB : (a : A) → (a' : A') → PA.R a a' → Param mB nB (B a) (B' a')) : Map0Has (R_forall PA PB)

Trocq Map0_forall.

Equations

• Transfer.Param.Map0_forall PA PB = { }

map1 — the univalence-free dependent-Π forward map

The dependent motive's forward transfer, axiom-free (only PA backward-map2a, no map4/univalence).

For each a' : A', set a := PA.bwd.map a'. The backward map_in_R at rfl gives a witness aR : PA.R a a'. The codomain family at that pair has a forward map (PB a a' aR).fwd.map : B a → B' a', applied to f a.

def Transfer.Param.Map1_forall {A A' : Type u} {B : A → Type u} {B' : A' → Type u} (PA : Param MapClass.map0 MapClass.map2a A A') (PB : (a : A) → (a' : A') → PA.R a a' → Param MapClass.map1 MapClass.map0 (B a) (B' a')) : Map1Has (R_forall PA PB)

Equations

• Transfer.Param.Map1_forall PA PB = { map := fun (f : (a : A) → B a) (a' : A') => (PB (PA.bwd.map a') a' ⋯).fwd.map (f (PA.bwd.map a')) }

Param-level assembly: the dependent-Π annotated relation at (map1, map0)

def Transfer.Param.paramForall {A A' : Type u} {B : A → Type u} {B' : A' → Type u} (PA : Param MapClass.map0 MapClass.map2a A A') (PB : (a : A) → (a' : A') → PA.R a a' → Param MapClass.map1 MapClass.map0 (B a) (B' a')) : Param MapClass.map1 MapClass.map0 ((a : A) → B a) ((a' : A') → B' a')

Assemble the dependent-Π Param from a domain Param02a and a Param10 codomain family: forward structure map1 (via Map1_forall), backward structure map0 (trivial). This is the level the univalence-free forward map supports — no map4/univalence used.

Equations

• Transfer.Param.paramForall PA PB = { R := Transfer.Param.R_forall PA PB, fwd := Transfer.Param.Map1_forall PA PB, bwd := { } }

Non-dependent corollary: recover the arrow relation

When B/B' are constant families, the dependent forall relation R_forall specialises to the (non-dependent) arrow relation: two functions are related when they send related inputs to related outputs. Here the codomain family is the constant family fun _ _ _ => PB.

def Transfer.Param.R_forall_const {A A' : Type u} {mA nA : MapClass} {C C' : Type u} (PA : Param mA nA A A') (PB : Param MapClass.map0 MapClass.map0 C C') : (A → C) → (A' → C') → Prop

The constant-family specialisation of R_forall over a flat codomain C, C'. This is definitionally the arrow relation fun f f' => ∀ a a' (_ : PA.R a a'), PB.R (f a) (f' a').

Equations

• Transfer.Param.R_forall_const PA PB = Transfer.Param.R_forall PA fun (x : A) (x_1 : A') (x_2 : PA.R x x_1) => PB

Demo: Map1_forall on a concrete family

A small end-to-end instantiation showing the forward map computes. Take the domain to be Unit related by full relation with a backward map, and a codomain family B a := Bool, B' a' := Bool related by equality, forward map := id. The forward dependent-Π map then transports a fun _ => true.

def Transfer.Param.paramUnit : Param MapClass.map0 MapClass.map2a Unit Unit

Diagonal domain Param on Unit: R = fun _ _ => True, forward map0, backward map2a with map := id and the trivial map_in_R.

Equations

• Transfer.Param.paramUnit = { R := fun (x x_1 : Unit) => True, fwd := { }, bwd := { map := fun (x : Unit) => (), map_in_R := ⋯ } }

def Transfer.Param.paramBoolFam (a a' : Unit) : paramUnit.R a a' → Param MapClass.map1 MapClass.map0 Bool Bool

Codomain family on Bool (equality graph), forward map1 with map := id, backward map0.

Equations

• Transfer.Param.paramBoolFam x✝² x✝¹ x✝ = { R := fun (b b' : Bool) => b = b', fwd := { map := id }, bwd := { } }