The dependent-pair (Σ) parametricity rule

The container rules of ParamData.lean (×, Option, List) lift a relation through non-dependent type formers. This file adds the dependent pair Σ a, B a: the type of the second component depends on the value of the first. It is the dependent generalization of the product × combinator, and the value-level companion of the dependent-Π rule in ParamForall.lean.

A dependent pair is related when the bases are related by PA and, at the induced witness, the fibers are related by the family PB — exactly the shape of the heterogeneous congruence hcongr_hetero (Congruence/HCongrConnection): the second projection of a related pair is a heterogeneous-congruence instance.

The AdapTT functor law

AdapTT (Adjedj–Lennon-Bertrand–Benjamin–Maillard, POPL 2026) makes type-cast adapters functorial over type formers: Adapt (F X) = F (Adapt X). For the dependent pair that law is sigma_cast_eq below — the Σ-cast is the pair of the base cast and the fiber cast. In AdapTT it holds definitionally (a cast calculus); here the forward map is built as that pair, so the law is rfl.

Unlike the non-dependent × (ParamData), the Σ-cast's second component depends on the witness produced by casting the first — so it needs the base relation at forward level map2a (a map whose graph is included in R, giving the witness), which is the univalence-free level. No map4/univalence is used: this is the value-level dependent former, below the universe.

The dependent-pair relation R_sigma

def Transfer.Param.R_sigma {A A' : Type u} {B : A → Type u} {B' : A' → Type u} {mA nA : MapClass} (PA : Param mA nA A A') (PB : (a : A) → (a' : A') → PA.R a a' → Param MapClass.map2a MapClass.map0 (B a) (B' a')) : (a : A) × B a → (a' : A') × B' a' → Prop

Two dependent pairs are related when their bases are PA-related (by some witness aR) and, at that witness, their fibers are (PB … aR)-related. The fiber relation is a family indexed by the base witness — the dependent analogue of the product relation R_prod. Only R fields are touched, so the base levels stay polymorphic.

Equations

• Transfer.Param.R_sigma PA PB p q = ∃ (aR : PA.R p.fst q.fst), (PB p.fst q.fst aR).R p.snd q.snd

The univalence-free forward map

Cast the base with PA.fwd.map, take the witness its graph provides (PA.fwd.map_in_R … rfl), and cast the fiber with the family's forward map at that witness. Needs the base forward at map2a (map + map_in_R) and the fiber forward at map2a (a map). No map4/univalence.

def Transfer.Param.Map1_sigma {A A' : Type u} {B : A → Type u} {B' : A' → Type u} {nA : MapClass} (PA : Param MapClass.map2a nA A A') (PB : (a : A) → (a' : A') → PA.R a a' → Param MapClass.map2a MapClass.map0 (B a) (B' a')) : Map1Has (R_sigma PA PB)

Equations

• Transfer.Param.Map1_sigma PA PB = { map := fun (p : (a : A) × B a) => ⟨PA.fwd.map p.fst, (PB p.fst (PA.fwd.map p.fst) ⋯).fwd.map p.snd⟩ }

Param-level assembly at (map1, map0)

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

The dependent-pair Param: forward structure map1 (via Map1_sigma), backward structure map0. This is the level the univalence-free forward map supports — the value-level dependent former, mirroring paramForall on the Π side.

Equations

• Transfer.Param.paramSigma PA PB = { R := Transfer.Param.R_sigma PA PB, fwd := Transfer.Param.Map1_sigma PA PB, bwd := { } }

The AdapTT functor law (cast form): Adapt (Σ) = Σ (Adapt)

theorem Transfer.Param.sigma_cast_eq {A A' : Type u} {B : A → Type u} {B' : A' → Type u} {nA : MapClass} (PA : Param MapClass.map2a nA A A') (PB : (a : A) → (a' : A') → PA.R a a' → Param MapClass.map2a MapClass.map0 (B a) (B' a')) (p : (a : A) × B a) : (paramSigma PA PB).fwd.map p = ⟨PA.fwd.map p.fst, (PB p.fst (PA.fwd.map p.fst) ⋯).fwd.map p.snd⟩

Functoriality of the dependent pair over the adapters. The Σ-cast is the pair of the base cast and the fiber cast: casting ⟨a, b⟩ yields ⟨cast a, cast b⟩ with the fiber cast taken at the witness the base cast induces. This is AdapTT's Adapt (Σ F) = Σ (Adapt F) in cast form — here rfl, because Map1_sigma is built as exactly that pair (in AdapTT it is a definitional cast-reduction rule). Univalence-free.

Demo: a dependent cast (Σ n, Fin (n+1) → Σ n, ℕ)

The fiber type Fin (n+1) depends on the base n, and the two sides' fibers are different types (Fin (n+1) vs ℕ), bridged by Fin.val. The Σ-cast carries the base unchanged and the fiber through Fin.val.

def Transfer.Param.natDomSigma : Param MapClass.map2a MapClass.map0 Nat Nat

Diagonal base on Nat at map2a (map := id, graph Eq).

Equations

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

def Transfer.Param.finValFib (a a' : Nat) : natDomSigma.R a a' → Param MapClass.map2a MapClass.map0 (Fin (a + 1)) Nat

Fiber family Fin (a+1) ↦ Nat at map2a, forward map Fin.val.

Equations

• Transfer.Param.finValFib x✝² x✝¹ x✝ = { R := fun (x : Fin (x✝² + 1)) (y : Nat) => ↑x = y, fwd := { map := Fin.val, map_in_R := ⋯ }, bwd := { } }

Composition (AdapTT AdaptComp for Σ)

Two Σ-transfers compose through the generic Param_trans machinery — no bespoke Σ-composition rule is needed. The composite Σ-cast is the composition of the two Σ-casts, so AdaptComp holds for the dependent pair as it does for →/×.

def Transfer.Param.paramSigmaTrans {X Y Z : Type u} (S₁ : Param MapClass.map1 MapClass.map0 X Y) (S₂ : Param MapClass.map1 MapClass.map0 Y Z) : Param MapClass.map1 MapClass.map0 X Z

Compose two dependent-pair transfers at (map1, map0) — the generic relation composition specialized to the level paramSigma produces.

Equations

• Transfer.Param.paramSigmaTrans S₁ S₂ = { R := Transfer.Param.R_trans S₁ S₂, fwd := Transfer.Param.Map1_trans S₁ S₂, bwd := { } }

theorem Transfer.Param.sigma_compose_cast {A B C : Type u} {BA : A → Type u} {BB : B → Type u} {BC : C → Type u} (PA : Param MapClass.map2a MapClass.map0 A B) (QA : Param MapClass.map2a MapClass.map0 B C) (PB : (a : A) → (b : B) → PA.R a b → Param MapClass.map2a MapClass.map0 (BA a) (BB b)) (QB : (b : B) → (c : C) → QA.R b c → Param MapClass.map2a MapClass.map0 (BB b) (BC c)) (p : (a : A) × BA a) : (paramSigmaTrans (paramSigma PA PB) (paramSigma QA QB)).fwd.map p = (paramSigma QA QB).fwd.map ((paramSigma PA PB).fwd.map p)

AdapTT AdaptComp for Σ. Casting through the composite of two dependent pairs equals casting through each in turn — the Σ-cast composes. rfl, because Map1_trans's forward map is the composition of the two forward maps.

Why composition goes through the maps, not a composed fiber family

The non-dependent product has a relational functor law ParamCoherence.prod_trans_rel: the composite relation equals the composite of the relations. Its dependent analogue would ask for a composed fiber family ∀ a c, (R_trans PA QA).R a c → Param .map2a .map0 (BA a) (BC c) — a Type-valued Param produced from the base's composed relation. But that relation is the existential glue ∃ b, PA.R a b ∧ QA.R b c, a Prop, and producing a Type from it is large elimination of Exists, which Lean forbids. So the dependent composition cannot be phrased as a composed fiber family over the glued base relation — it must compose the Params (which carry the fibers as data), as paramSigmaTrans does. This is a shadow of the same Prop/Type boundary that caps the universe fiber (map4) by UnivalenceStatus.univalence_inconsistent.