The arrow (app / function) parametricity rule

A Lean port of Trocq's std/Param_arrow.v (https://github.com/rocq-community/trocq): the combinators that build a Param annotated relation on a function space (A → B) from Param relations on the domain A and codomain B.

This is the function rule of the parametricity translation: it tells the engine how to relate f : A → B and f' : A' → B'.

The funext advantage

Coq's std variant gates the map2b/map3 arrow combinators on a `{Funext} instance, because their R_in_map field needs functional extensionality to prove map f = f' from a pointwise relation. Lean has funext as a theorem, so those gates are unnecessary: map0 through map3 (and map4, free by proof irrelevance on Prop-valued R) hold with no extra axioms.

Accessor dictionary (Coq → Lean)

At the input levels where the field exists:

• map PB → PB.fwd.map (PB fwd ≥ map1)
• comap PA → PA.bwd.map (PA bwd ≥ map1)
• map_in_R PB → PB.fwd.map_in_R (PB fwd ≥ map2a)
• R_in_map PB → PB.fwd.R_in_map (PB fwd ≥ map2b)
• comap_in_R PA → PA.bwd.map_in_R (PA bwd ≥ map2a)
• R_in_comap PA → PA.bwd.R_in_map (PA bwd ≥ map2b)

Recall PA.bwd : MapHas n (symRel PA.R), and symRel PA.R a' a = PA.R a a', so PA.bwd.map : A' → A, PA.bwd.map_in_R : ∀ a' a, PA.bwd.map a' = a → PA.R a a', and PA.bwd.R_in_map : ∀ a' a, PA.R a a' → PA.bwd.map a' = a.

The function relation R_arrow

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

Trocq R_arrow: two functions are related when they send PA-related inputs to PB-related outputs. Coq accesses only the R field, so the level parameters stay fully polymorphic (the function relation does not depend on how much structure each component carries).

Equations

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

map0 — no structure

def Transfer.Param.Map0_arrow {A A' B B' : Type u} {mA nA mB nB : MapClass} (PA : Param mA nA A A') (PB : Param mB nB B B') : Map0Has (R_arrow PA PB)

Trocq Map0_arrow.

Equations

• Transfer.Param.Map0_arrow PA PB = { }

map1 — the forward map PB.map ∘ f ∘ PA.comap

def Transfer.Param.Map1_arrow {A A' B B' : Type u} (PA : Param MapClass.map0 MapClass.map1 A A') (PB : Param MapClass.map1 MapClass.map0 B B') : Map1Has (R_arrow PA PB)

Trocq Map1_arrow: the function map sends f : A → B to fun a' => PB.fwd.map (f (PA.bwd.map a')). Needs PA backward-map1 (to get comap) and PB forward-map1 (to get map).

Equations

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

map2a — map plus graph-inclusion map_in_R

def Transfer.Param.Map2a_arrow {A A' B B' : Type u} (PA : Param MapClass.map0 MapClass.map2b A A') (PB : Param MapClass.map2a MapClass.map0 B B') : Map2aHas (R_arrow PA PB)

Trocq Map2a_arrow. The function map is the same PB.map ∘ f ∘ PA.comap; map_in_R says: if that map sends f to f', then f and f' are R_arrow-related. Needs PA backward-map2b (R_in_comap) and PB forward-map2a (map_in_R).

Equations

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

map2b — map plus relation-inclusion R_in_map (via funext)

def Transfer.Param.Map2b_arrow {A A' B B' : Type u} (PA : Param MapClass.map0 MapClass.map2a A A') (PB : Param MapClass.map2b MapClass.map0 B B') : Map2bHas (R_arrow PA PB)

Trocq Map2b_arrow. R_in_map says: if f, f' are R_arrow-related, then the function map sends f to f'. The Coq std variant gates this on `{Funext}; in Lean funext is a theorem, so it is axiom-free. Needs PA backward-map2a (comap_in_R) and PB forward-map2b (R_in_map).

Equations

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

map3 — both inclusions (via funext)

def Transfer.Param.Map3_arrow {A A' B B' : Type u} (PA : Param MapClass.map0 MapClass.map3 A A') (PB : Param MapClass.map3 MapClass.map0 B B') : Map3Has (R_arrow PA PB)

Trocq Map3_arrow: the full graph relation, combining Map2a_arrow's map_in_R and Map2b_arrow's R_in_map. Needs both inclusions on each component: PA backward-map3, PB forward-map3. Axiom-free in Lean (the R_in_map half uses funext).

Equations

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

map4 — map3 plus the (free, proof-irrelevant) coherence

def Transfer.Param.Map4_arrow {A A' B B' : Type u} (PA : Param MapClass.map0 MapClass.map3 A A') (PB : Param MapClass.map3 MapClass.map0 B B') : Map4Has (R_arrow PA PB)

Trocq Map4_arrow. Over Prop-valued R the coherence R_in_mapK is automatic by proof irrelevance, so the univalent level is constructible without univalence. Needs PA backward-map3, PB forward-map3.

Equations

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

The Param-level arrow combinator

Assembling forward and backward structure into a Param on the function space. The forward-map1, backward-map1 output needs only a forward and a backward map on each component, i.e. PA PB : Param .map1 .map1.

• The forward map is Map1_arrow's PB.map ∘ · ∘ PA.comap.
• The backward map is the symmetric PA.map ∘ · ∘ PB.comap — Map1_arrow run on the directions of PA.symm, PB.symm. Since Map1Has (and hence the bwd field MapHas .map1 (symRel (R_arrow PA PB))) records only a function, it is built inline and no relation-coercion is needed.

def Transfer.Param.paramArrow {A A' B B' : Type u} (PA : Param MapClass.map1 MapClass.map1 A A') (PB : Param MapClass.map1 MapClass.map1 B B') : Param MapClass.map1 MapClass.map1 (A → B) (A' → B')

paramArrow: from PA PB : Param .map1 .map1, an annotated relation Param .map1 .map1 (A → B) (A' → B') whose relation is R_arrow PA PB, forward map PB.map ∘ · ∘ PA.comap, backward map PA.map ∘ · ∘ PB.comap.

Equations

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

Demo: the arrow combinators compose on a concrete pair

The identity (equality) relation on a type, packaged at the levels each arrow rule consumes (Param .map0 .map3 as domain, Param .map3 .map0 as codomain, Param .map1 .map1 for paramArrow), feeds two copies through the arrow combinators; the resulting function relation is the pointwise lift of equality.

def Transfer.Param.paramEqDom (T : Type u) : Param MapClass.map0 MapClass.map3 T T

The diagonal as a domain input for the arrow rules: forward-map0, backward-map3.

Equations

• Transfer.Param.paramEqDom T = { R := Eq, fwd := { }, bwd := { map := id, map_in_R := ⋯, R_in_map := ⋯ } }

def Transfer.Param.paramEqCod (S : Type u) : Param MapClass.map3 MapClass.map0 S S

The diagonal as a codomain input for the arrow rules: forward-map3, backward-map0.

Equations

• Transfer.Param.paramEqCod S = { R := Eq, fwd := { map := id, map_in_R := ⋯, R_in_map := ⋯ }, bwd := { } }

def Transfer.Param.paramEq1 (T : Type u) : Param MapClass.map1 MapClass.map1 T T

The diagonal at the forward-map1, backward-map1 level (the input shape paramArrow consumes).

Equations

• Transfer.Param.paramEq1 T = { R := Eq, fwd := { map := id }, bwd := { map := id } }