Relation composition (Param_trans)

A Lean port of Trocq's std/generic/Param_trans.v (https://github.com/rocq-community/trocq) — the rule that composes two annotated relations Param m n A B and Param m n B C into one on A C. It is the transitivity half of the relational-PER structure (Param.symm in ParamHierarchy.lean is the symmetry half), and the mechanism behind the paper's bitvector-encoding chaining (A ↪ B ↪ C).

The composite relation

For R : A → B → Prop and S : B → C → Prop the composite is the usual existential glue

R_trans R S a c := ∃ b, R a b ∧ S b c

(Coq's Param_trans uses the Σ-glued relation; over Prop-valued R the ∃ form is the right one — proof irrelevance collapses the choice of witness that would otherwise matter at map4.)

Which classes compose

The forward map of the composite is the function composition S.map ∘ R.map, and every MapHas field lifts without univalence:

level	forward field	how it lifts
map0	(none)	trivial
map1	map	S.fwd.map ∘ R.fwd.map
map2a	map_in_R	witness b := R.map a, then chase both inclusions
map2b	R_in_map	R.R_in_map then S.R_in_map (no funext needed: maps, not functions)
map3	both	combine the two above

So Param_trans covers map0–map3 in both directions (the backward direction is the same construction on symRel, which is itself a composition — symRel (R_trans R S) = R_trans (symRel S) (symRel R), the order flips). The map4 coherence R_in_mapK is the only field that does not compose for free even on Prop: the round-trip map_in_R (R_in_map r) of the composite mixes the two witnesses, and recovering r needs the equivalence coherence (univalence territory). So map0–map3 are fully proved and map4 is documented as the residual, exactly as the arrow/forall/data rules do.

The composite relation R_trans (Coq Param_trans relation)

def Transfer.Param.R_trans {A B C : Type u} {mR nR mS nS : MapClass} (P : Param mR nR A B) (Q : Param mS nS B C) : A → C → Prop

Trocq composite relation: a relates to c when there is an intermediate b with R a b and S b c. The level parameters stay polymorphic — the relation touches only the R fields.

Equations

• Transfer.Param.R_trans P Q a c = ∃ (b : B), P.R a b ∧ Q.R b c

theorem Transfer.Param.symRel_R_trans {A B C : Type u} {mR nR mS nS : MapClass} (P : Param mR nR A B) (Q : Param mS nS B C) : symRel (R_trans P Q) = fun (c : C) (a : A) => ∃ (b : B), Q.R b c ∧ P.R a b

The flip of a composite is the composite of the flips, with order reversed: symRel (R_trans P Q) = R_trans (symRel S) (symRel R). This is the bookkeeping lemma that lets the backward map reuse the same forward construction.

The forward MapHas records compose (map0–map3)

def Transfer.Param.Map0_trans {A B C : Type u} {mR nR mS nS : MapClass} (P : Param mR nR A B) (Q : Param mS nS B C) : Map0Has (R_trans P Q)

map0: nothing to compose.

Equations

• Transfer.Param.Map0_trans P Q = { }

def Transfer.Param.Map1_trans {A B C : Type u} {nR nS : MapClass} (P : Param MapClass.map1 nR A B) (Q : Param MapClass.map1 nS B C) : Map1Has (R_trans P Q)

map1: the forward map of the composite is S.map ∘ R.map. Needs both forward maps.

Equations

• Transfer.Param.Map1_trans P Q = { map := fun (a : A) => Q.fwd.map (P.fwd.map a) }

def Transfer.Param.Map2a_trans {A B C : Type u} {nR nS : MapClass} (P : Param MapClass.map2a nR A B) (Q : Param MapClass.map2a nS B C) : Map2aHas (R_trans P Q)

map2a: the composite map's graph is included in R_trans. Pick the intermediate witness b := R.map a; then R a b by R.map_in_R rfl, and S b c by S.map_in_R (since S.map b = c). Needs both forward map2a.

Equations

• Transfer.Param.Map2a_trans P Q = { map := fun (a : A) => Q.fwd.map (P.fwd.map a), map_in_R := ⋯ }

def Transfer.Param.Map2b_trans {A B C : Type u} {nR nS : MapClass} (P : Param MapClass.map2b nR A B) (Q : Param MapClass.map2b nS B C) : Map2bHas (R_trans P Q)

map2b: R_trans-relatedness implies the composite map sends a to c. From the witness b: R.R_in_map gives R.map a = b, S.R_in_map gives S.map b = c; compose. No funext is needed — these are maps on data, not function spaces, so this lifts univalence-free (unlike Coq's funext gate on the arrow rule). Needs both forward map2b.

Equations

• Transfer.Param.Map2b_trans P Q = { map := fun (a : A) => Q.fwd.map (P.fwd.map a), R_in_map := ⋯ }

def Transfer.Param.Map3_trans {A B C : Type u} {nR nS : MapClass} (P : Param MapClass.map3 nR A B) (Q : Param MapClass.map3 nS B C) : Map3Has (R_trans P Q)

map3: both inclusions; the composite is the graph of S.map ∘ R.map. Needs both forward map3.

Equations

• Transfer.Param.Map3_trans P Q = { map := fun (a : A) => Q.fwd.map (P.fwd.map a), map_in_R := ⋯, R_in_map := ⋯ }

The backward records compose

symRel (R_trans P Q) is the composite of the flipped relations (in reverse order). The backward MapHas is therefore built from Q.bwd then P.bwd, mirroring the forward construction. The map0–map3 backward builders are parameterised by the backward levels.

def Transfer.Param.Map1_trans_bwd {A B C : Type u} {mR mS : MapClass} (P : Param mR MapClass.map1 A B) (Q : Param mS MapClass.map1 B C) : Map1Has (symRel (R_trans P Q))

Backward map1: the backward map of the composite is R.comap ∘ S.comap (the flip of S.map ∘ R.map). Needs both backward maps.

Equations

• Transfer.Param.Map1_trans_bwd P Q = { map := fun (c : C) => P.bwd.map (Q.bwd.map c) }

def Transfer.Param.Map2a_trans_bwd {A B C : Type u} {mR mS : MapClass} (P : Param mR MapClass.map2a A B) (Q : Param mS MapClass.map2a B C) : Map2aHas (symRel (R_trans P Q))

Backward map2a. P.bwd : MapHas .map2a (symRel P.R), so P.bwd.map : B → A and P.bwd.map_in_R : ∀ b a, P.bwd.map b = a → P.R a b. Pick the witness b := S.comap c. Needs both backward map2a.

Equations

• Transfer.Param.Map2a_trans_bwd P Q = { map := fun (c : C) => P.bwd.map (Q.bwd.map c), map_in_R := ⋯ }

def Transfer.Param.Map2b_trans_bwd {A B C : Type u} {mR mS : MapClass} (P : Param mR MapClass.map2b A B) (Q : Param mS MapClass.map2b B C) : Map2bHas (symRel (R_trans P Q))

Backward map2b. P.bwd.R_in_map : ∀ b a, P.R a b → P.bwd.map b = a. Needs both backward map2b.

Equations

• Transfer.Param.Map2b_trans_bwd P Q = { map := fun (c : C) => P.bwd.map (Q.bwd.map c), R_in_map := ⋯ }

def Transfer.Param.Map3_trans_bwd {A B C : Type u} {mR mS : MapClass} (P : Param mR MapClass.map3 A B) (Q : Param mS MapClass.map3 B C) : Map3Has (symRel (R_trans P Q))

Backward map3.

Equations

• Transfer.Param.Map3_trans_bwd P Q = { map := fun (c : C) => P.bwd.map (Q.bwd.map c), map_in_R := ⋯, R_in_map := ⋯ }

Param_trans: the composition combinator

The combinator is exposed at the four diagonal levels map0–map3 (forward and backward equal), the shape the chaining demo and the registry use. Off-diagonal mixes (Param m n with m ≠ n) compose by the same field builders above with the appropriate level arguments; the diagonal instances are the canonical entry points (with Param_trans_map3_map0, the embedding-chaining shape, given explicitly).

def Transfer.Param.Param_trans_map0 {A B C : Type u} (P : Param MapClass.map0 MapClass.map0 A B) (Q : Param MapClass.map0 MapClass.map0 B C) : Param MapClass.map0 MapClass.map0 A C

Param_trans at map0 — relation composition with no structure.

Equations

• Transfer.Param.Param_trans_map0 P Q = { R := Transfer.Param.R_trans P Q, fwd := { }, bwd := { } }

def Transfer.Param.Param_trans_map1 {A B C : Type u} (P : Param MapClass.map1 MapClass.map1 A B) (Q : Param MapClass.map1 MapClass.map1 B C) : Param MapClass.map1 MapClass.map1 A C

Param_trans at map1 — compose two forward+backward maps.

Equations

• Transfer.Param.Param_trans_map1 P Q = { R := Transfer.Param.R_trans P Q, fwd := Transfer.Param.Map1_trans P Q, bwd := Transfer.Param.Map1_trans_bwd P Q }

def Transfer.Param.Param_trans_map2a {A B C : Type u} (P : Param MapClass.map2a MapClass.map2a A B) (Q : Param MapClass.map2a MapClass.map2a B C) : Param MapClass.map2a MapClass.map2a A C

Param_trans at map2a — compose graph-inclusions both ways.

Equations

• Transfer.Param.Param_trans_map2a P Q = { R := Transfer.Param.R_trans P Q, fwd := Transfer.Param.Map2a_trans P Q, bwd := Transfer.Param.Map2a_trans_bwd P Q }

def Transfer.Param.Param_trans_map2b {A B C : Type u} (P : Param MapClass.map2b MapClass.map2b A B) (Q : Param MapClass.map2b MapClass.map2b B C) : Param MapClass.map2b MapClass.map2b A C

Param_trans at map2b — compose relation-inclusions both ways.

Equations

• Transfer.Param.Param_trans_map2b P Q = { R := Transfer.Param.R_trans P Q, fwd := Transfer.Param.Map2b_trans P Q, bwd := Transfer.Param.Map2b_trans_bwd P Q }

def Transfer.Param.Param_trans_map3 {A B C : Type u} (P : Param MapClass.map3 MapClass.map3 A B) (Q : Param MapClass.map3 MapClass.map3 B C) : Param MapClass.map3 MapClass.map3 A C

Param_trans at map3 — the composite of two full graph relations is itself a full graph relation, in both directions, univalence-free.

Equations

• Transfer.Param.Param_trans_map3 P Q = { R := Transfer.Param.R_trans P Q, fwd := Transfer.Param.Map3_trans P Q, bwd := Transfer.Param.Map3_trans_bwd P Q }

def Transfer.Param.Param_trans_map3_map0 {A B C : Type u} (P : Param MapClass.map3 MapClass.map0 A B) (Q : Param MapClass.map3 MapClass.map0 B C) : Param MapClass.map3 MapClass.map0 A C

Param_trans for the embedding shape map3 / map0 — the exact level of paramOfEmbedding/paramOfEquiv-without-decoder. Composing two encodings A ↪ B ↪ C yields the chained encoding A ↪ C (forward map3, backward map0), the paper's bitvector-chaining pattern.

Equations

• Transfer.Param.Param_trans_map3_map0 P Q = { R := Transfer.Param.R_trans P Q, fwd := Transfer.Param.Map3_trans P Q, bwd := { } }

Demos: chaining registered relations

def Transfer.Param.paramChainEmbed {A α β : Type u} [ReprEmbeddingClass A α] [ReprEmbeddingClass α β] : Param MapClass.map3 MapClass.map0 A β

Chaining two ReprEmbeddingClass encodings A ↪ α ↪ β into a single annotated relation A ↔ β (forward map3, backward map0) — the bitvector-chaining pattern: encode through an intermediate representation, then through the final one.

Equations

• Transfer.Param.paramChainEmbed = Transfer.Param.Param_trans_map3_map0 Transfer.Param.paramOfEmbedding Transfer.Param.paramOfEmbedding

Diagonal (equality) chaining — A ≃ B ≃ C style at map3

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

The diagonal at full map3 both ways: Eq is the graph of id, with both inclusions identities.

Equations

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