The coherence-law suite (functor laws)

The combinators in ParamTrans/ParamArrow/ParamData build annotated relations; this file proves the coherence laws that govern how they compose. These are the Lean realizations of the laws of AdapTT (Adjedj, Lennon-Bertrand, Benjamin, Maillard, AdapTT: Functoriality for Dependent Type Casts, POPL 2026): the cast-adapter identity AdaptId and composition AdaptComp, plus the functoriality of each type former over those adapters. AdapTT secures them definitionally via a bespoke cast calculus. In Lean the cast-form laws (cast_id/cast_trans) hold by rfl for free — the composite's forward map is already function composition, so composition through nested type formers is automatic and the "stuck adapter" gap Trocq's stuck.v documents does not arise; they need not be cited, but they certify the functor laws hold, and are used explicitly where a coercion chain is built by hand (e.g. a transport along a chain of intermediate representations). The relational-form law (prod_trans_rel) is the one proved propositionally (funext/propext). The dependent type formers extend the non-dependent →/×/List/Option laws here: paramForall (Π, ParamForall.lean) and paramSigma (Σ, ParamSigma.lean, sigma_cast_eq = Adapt Σ = Σ Adapt) carry the same functoriality into the dependent world.

Contents

1. Cast-composition (AdaptComp/AdaptId). castViaParam P a := P.fwd.map a is the representation-change coercion. cast_trans and cast_id are the two coherence laws that make coercion chains correct; both hold by rfl because Param_trans's forward map is Q.map ∘ P.map and paramId's is id.

2. Combinator distributes over composition (the functor law), forward-map / cast form. For each container/type-former combinator, the forward map of "compose then combine" equals "combine then compose" — the cast/forward-map version of the functor law (prod, option, list, arrow). For arrow this is contravariant in the domain.

3. Combinator-distributes, full relational form. Proved for prod (the relation of the composite equals the composite of the relations) via funext/propext. arrow/sum/option/list relational forms are noted where they need more than the cast form.

4. Identity laws (cast form). prod_id/arrow_id: a combinator applied to identity Params acts as the identity coercion.

All laws are univalence-free: they live entirely in the map1–map3 forward fragment, exactly the fragment ParamHierarchy's module docstring marks as axiom-free in Lean (funext is a theorem; only the map4 universe relation needs univalence).

1. Cast-composition: AdapTT AdaptId / AdaptComp

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

The identity annotated relation on T: relation Eq, both maps id, full map3 in both directions. The diagonal Param. (Same data as paramEqFull; named paramId to flag its role as the unit of the composition Param_trans.)

Equations

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

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

The identity annotated relation at the forward/backward-map1 level — the input shape paramArrow consumes. Relation Eq, both maps id.

Equations

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

def Transfer.Param.paramIdElt (T : Type u) : Param MapClass.map2a MapClass.map0 T T

The identity annotated relation at the forward-map2a, backward-map0 level — the input shape paramProd/paramOption/paramList consume. Relation Eq, forward map id (its graph is Eq).

Equations

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

def Transfer.Param.castViaParam {A B : Type u} {n : MapClass} (P : Param MapClass.map3 n A B) (a : A) : B

Representation-change coercion induced by a Param: its forward map. The forward level is map3 (the level paramId and Param_trans_map3 produce); the backward level stays polymorphic.

Equations

• Transfer.Param.castViaParam P a = P.fwd.map a

theorem Transfer.Param.cast_trans {A B C : Type u} (P : Param MapClass.map3 MapClass.map3 A B) (Q : Param MapClass.map3 MapClass.map3 B C) (a : A) : castViaParam (Param_trans_map3 P Q) a = castViaParam Q (castViaParam P a)

AdaptComp — coercion through a composite relation is the composition of the two coercions. Holds by rfl: Param_trans_map3's forward map is Q.fwd.map ∘ P.fwd.map. This is the law that makes a coercion chain (abstract → bytes → field) correct.

theorem Transfer.Param.cast_id {A : Type u} (a : A) : castViaParam (paramId A) a = a

AdaptId — coercion through the identity relation is the identity. Holds by rfl: paramId's forward map is id.

Composing element Params at the level the data combinators consume

paramProd/paramOption/paramList consume Param .map2a .map0. Their two-step composite is again a Param .map2a .map0, built from Map2a_trans's forward record (the backward direction is map0, nothing to compose). This is the data-rule instance of Param_trans.

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

Compose two element Params at the forward-map2a, backward-map0 level — the shape the data combinators consume. Forward map is Q.map ∘ P.map.

Equations

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

theorem Transfer.Param.Param_trans_map2a_map0_map {A B C : Type u} (P : Param MapClass.map2a MapClass.map0 A B) (Q : Param MapClass.map2a MapClass.map0 B C) (a : A) : (Param_trans_map2a_map0 P Q).fwd.map a = Q.fwd.map (P.fwd.map a)

Its forward map is the function composition (definitional).

2. Functor law, cast / forward-map form

For each combinator: the forward map of composing two combinator-built Params equals the combinator applied to the composed argument-Params. This is the AdapTT type-former functoriality (Adapt (F …) = F (Adapt …)) in its cast form. The data combinators consume Param .map2a .map0; the arrow combinator consumes Param .map1 .map1. The forward maps are function compositions, so each law is rfl (or cases+rfl / simp through the recursive lift).

Product (covariant in both arguments)

theorem Transfer.Param.prod_trans_cast {A B C : Type u} (PA : Param MapClass.map2a MapClass.map0 A B) (QA : Param MapClass.map2a MapClass.map0 B C) (PB : Param MapClass.map2a MapClass.map0 A B) (QB : Param MapClass.map2a MapClass.map0 B C) (p : A × A) : (paramProd (Param_trans_map2a_map0 PA QA) (Param_trans_map2a_map0 PB QB)).fwd.map p = (paramProd QA QB).fwd.map ((paramProd PA PB).fwd.map p)

prod_trans (cast form). The forward map of the product of two composite element relations equals the composite of the two product forward maps: prod_map (Q∘P) = prod_map Q ∘ prod_map P, componentwise.

Option / List (covariant)

theorem Transfer.Param.option_trans_cast {A B C : Type u} (PA : Param MapClass.map2a MapClass.map0 A B) (QA : Param MapClass.map2a MapClass.map0 B C) (o : Option A) : (paramOption (Param_trans_map2a_map0 PA QA)).fwd.map o = (paramOption QA).fwd.map ((paramOption PA).fwd.map o)

option_trans (cast form). Option.map (Q∘P) = Option.map Q ∘ Option.map P on the lifted relations.

theorem Transfer.Param.list_trans_cast {A B C : Type u} (PA : Param MapClass.map2a MapClass.map0 A B) (QA : Param MapClass.map2a MapClass.map0 B C) (l : List A) : (paramList (Param_trans_map2a_map0 PA QA)).fwd.map l = (paramList QA).fwd.map ((paramList PA).fwd.map l)

list_trans (cast form). List.map (Q∘P) = List.map Q ∘ List.map P on the lifted relations.

Arrow (contravariant in the domain)

paramArrow PA PB has forward map fun f a' => PB.fwd.map (f (PA.bwd.map a')). Composing two arrows, the codomain maps compose forward (PB) while the domain backward maps compose in the reverse order (PA) — the contravariance. The Param_trans_map3 of the domain supplies a backward map P.bwd.map ∘ Q.bwd.map (reversed), exactly matching the conjugation order, so the law is rfl.

theorem Transfer.Param.arrow_trans_cast {A B C : Type u} (PA : Param MapClass.map1 MapClass.map1 A B) (QA : Param MapClass.map1 MapClass.map1 B C) (PB : Param MapClass.map1 MapClass.map1 A B) (QB : Param MapClass.map1 MapClass.map1 B C) (f : A → A) (c : C) : (paramArrow (Param_trans_map1 PA QA) (Param_trans_map1 PB QB)).fwd.map f c = (paramArrow QA QB).fwd.map ((paramArrow PA PB).fwd.map f) c

arrow_trans (cast form). The forward map of the composite of two arrow Params equals the arrow combinator applied to the composed domain/codomain Params — with the domain composed contravariantly. Both sides send f : A → A to the conjugation (QB∘PB) ∘ f ∘ (P_A.bwd ∘ Q_A.bwd).

3. Functor law, full relational form (product)

theorem Transfer.Param.prod_trans_rel {A B C : Type u} (PA : Param MapClass.map2a MapClass.map0 A B) (QA : Param MapClass.map2a MapClass.map0 B C) (PB : Param MapClass.map2a MapClass.map0 A B) (QB : Param MapClass.map2a MapClass.map0 B C) : R_prod (Param_trans_map2a_map0 PA QA) (Param_trans_map2a_map0 PB QB) = R_trans (paramProd PA PB) (paramProd QA QB)

prod_trans (relational form). The relation of the product of two composite element relations equals (as a relation, via funext/propext) the composite of the two product relations. This is the strict functor law R_prod (Q∘P) = (R_prod Q) ∘ (R_prod P) for the product type former.

Left side: (a,b) ~ (c,d) iff ∃ m, PA.R a m ∧ QA.R m c and likewise on the second component (two independent witnesses). Right side: one shared witness pair (m₁,m₂). They agree because the product witness can be split/paired.

4. Identity laws (cast form): combinator over paramId = identity coercion

theorem Transfer.Param.prod_id_cast {A : Type u} (p : A × A) : (paramProd (paramIdElt A) (paramIdElt A)).fwd.map p = p

prod_id. The product combinator applied to two identity element Params has forward map the identity on the product.

theorem Transfer.Param.arrow_id_cast {A : Type u} (f : A → A) : (paramArrow (paramId1 A) (paramId1 A)).fwd.map f = f

arrow_id. The arrow combinator applied to identity domain and codomain Params has forward map the identity on the function space (up to funext): conjugating by id on both sides is the identity.

Demos: the coherence laws close, and one combinator law