The Param relation hierarchy

A faithful Lean port of Trocq's level lattice (rocq-community/trocq, std/Hierarchy.v) — the std (non-HoTT) variant, the appropriate one for Lean+Mathlib.

map_class := map0 | map1 | map2a | map2b | map3 | map4 records how much structure a relation R : A → B → Prop carries in one direction:

level	fields of Map_k.Has R
map0	(none)
map1	map : A → B
map2a	map, map_in_R : map a = b → R a b
map2b	map, R_in_map : R a b → map a = b
map3	map, map_in_R, R_in_map
map4	map3 + coherence R_in_mapK (automatic here by proof irrelevance)

A Param m n A B packages a relation R with a Map_m.Has R (forward) and a Map_n.Has (sym R) (backward) — Trocq's annotated relation (m,n).

Prop-valued relations and funext

The relations are R : A → B → Prop (the equation-style relations the crypto transfer uses); the Type-valued generalization (needed for the universe / dependent-Type motive) is noted where it applies. Lean has funext as a theorem, so the combinators Coq's std had to gate on `{Funext} (map2b/map3 arrow/forall) are axiom-free here — only the map4 universe relation needs univalence. The univalence-free fragment is thus map0–map3 in every component, wider than the paper's {0,1,2a}. With Prop-valued R, proof irrelevance makes the map4 coherence R_in_mapK automatic, so even Map4.Has is constructible for these relations.

The level lattice

inductive Transfer.Param.MapClass : Type

Trocq's map_class (std/Hierarchy.v): the six structure levels a relation can carry in one direction.

• map0 : MapClass
• map1 : MapClass
• map2a : MapClass
• map2b : MapClass
• map3 : MapClass
• map4 : MapClass

@[instance_reducible]

instance Transfer.Param.instDecidableEqMapClass : DecidableEq MapClass

Equations

• Transfer.Param.instDecidableEqMapClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Transfer.Param.instReprMapClass : Repr MapClass

Equations

• Transfer.Param.instReprMapClass = { reprPrec := Transfer.Param.instReprMapClass.repr }

def Transfer.Param.instReprMapClass.repr : MapClass → Nat → Std.Format

Equations

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

The Map_k.Has R records (ported from std/Hierarchy.v)

structure Transfer.Param.Map0Has {A B : Type u} (R : A → B → Prop) : Type u

map0: no structure.

structure Transfer.Param.Map1Has {A B : Type u} (R : A → B → Prop) : Type u

map1: a forward map.

• map : A → B

structure Transfer.Param.Map2aHas {A B : Type u} (R : A → B → Prop) : Type u

map2a: a map whose graph is included in R.

• map : A → B
• map_in_R (a : A) (b : B) : self.map a = b → R a b

structure Transfer.Param.Map2bHas {A B : Type u} (R : A → B → Prop) : Type u

map2b: a map that includes R (so R is single-valued through map).

• map : A → B
• R_in_map (a : A) (b : B) : R a b → self.map a = b

structure Transfer.Param.Map3Has {A B : Type u} (R : A → B → Prop) : Type u

map3: R is exactly the graph of map (both inclusions).

• map : A → B
• map_in_R (a : A) (b : B) : self.map a = b → R a b
• R_in_map (a : A) (b : B) : R a b → self.map a = b

structure Transfer.Param.Map4Has {A B : Type u} (R : A → B → Prop) : Type u

map4: map3 + the coherence R_in_mapK. For Prop-valued R the coherence is automatic (proof irrelevance), so this is map3 + a free field — a faithful placeholder for the univalent level (which over Type-valued R is the equivalence-coherence requiring univalence).

• map : A → B
• map_in_R (a : A) (b : B) : self.map a = b → R a b
• R_in_map (a : A) (b : B) : R a b → self.map a = b
• R_in_mapK (a : A) (b : B) (r : R a b) : ⋯ = r

def Transfer.Param.MapHas {A B : Type u} : MapClass → (A → B → Prop) → Type u

The Map_k.Has record type indexed by the level.

Equations

• Transfer.Param.MapHas Transfer.Param.MapClass.map0 x✝ = Transfer.Param.Map0Has x✝
• Transfer.Param.MapHas Transfer.Param.MapClass.map1 x✝ = Transfer.Param.Map1Has x✝
• Transfer.Param.MapHas Transfer.Param.MapClass.map2a x✝ = Transfer.Param.Map2aHas x✝
• Transfer.Param.MapHas Transfer.Param.MapClass.map2b x✝ = Transfer.Param.Map2bHas x✝
• Transfer.Param.MapHas Transfer.Param.MapClass.map3 x✝ = Transfer.Param.Map3Has x✝
• Transfer.Param.MapHas Transfer.Param.MapClass.map4 x✝ = Transfer.Param.Map4Has x✝

The annotated relation Param (m,n)

@[reducible, inline]

abbrev Transfer.Param.symRel {A B : Type u} (R : A → B → Prop) : B → A → Prop

The flipped relation.

Equations

• Transfer.Param.symRel R b a = R a b

structure Transfer.Param.Param (m n : MapClass) (A B : Type u) : Type u

Param m n A B: a relation R with forward structure Map_m.Has R and backward structure Map_n.Has (sym R) — Trocq's annotated relation.

• R : A → B → Prop
• fwd : MapHas m self.R
• bwd : MapHas n (symRel self.R)

def Transfer.Param.Param.symm {m n : MapClass} {A B : Type u} (p : Param m n A B) : Param n m B A

Symmetry (the data is symmetric): swap directions.

Equations

• p.symm = { R := Transfer.Param.symRel p.R, fwd := p.bwd, bwd := p.fwd }

Weakening (the lattice order): forget structure

def Transfer.Param.Map1Has.forget {A B : Type u} {R : A → B → Prop} : Map1Has R → Map0Has R

map1 → map0.

Equations

• x✝.forget = { }

def Transfer.Param.Map2aHas.toMap1 {A B : Type u} {R : A → B → Prop} (h : Map2aHas R) : Map1Has R

map2a → map1.

Equations

• h.toMap1 = { map := h.map }

def Transfer.Param.Map2bHas.toMap1 {A B : Type u} {R : A → B → Prop} (h : Map2bHas R) : Map1Has R

map2b → map1.

Equations

• h.toMap1 = { map := h.map }

def Transfer.Param.Map3Has.toMap2a {A B : Type u} {R : A → B → Prop} (h : Map3Has R) : Map2aHas R

map3 → map2a.

Equations

• h.toMap2a = { map := h.map, map_in_R := ⋯ }

def Transfer.Param.Map3Has.toMap2b {A B : Type u} {R : A → B → Prop} (h : Map3Has R) : Map2bHas R

map3 → map2b.

Equations

• h.toMap2b = { map := h.map, R_in_map := ⋯ }

def Transfer.Param.Map4Has.toMap3 {A B : Type u} {R : A → B → Prop} (h : Map4Has R) : Map3Has R

map4 → map3.

Equations

• h.toMap3 = { map := h.map, map_in_R := ⋯, R_in_map := ⋯ }

Bridge: ReprEmbeddingClass is a Param

The encoding enc : A → α with its graph R a b := enc a = b is forward-map3 (the graph makes both inclusions identities); without a decoder the backward direction is map0. So an embedding is a Param map3 map0.

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

An embedding A ↪ α (graph of enc) as a forward-map3, backward-map0 annotated relation.

Equations

• Transfer.Param.paramOfEmbedding = { R := fun (a : A) (b : α) => Transfer.ReprMapClass.enc a = b, fwd := { map := Transfer.ReprMapClass.enc, map_in_R := ⋯, R_in_map := ⋯ }, bwd := { } }

def Transfer.Param.paramOfMap {A α : Type u} [ReprMapClass A α] : Param MapClass.map1 MapClass.map0 A α

A bare representation map as a forward-map1, backward-map0 relation.

Equations

• Transfer.Param.paramOfMap = { R := fun (a : A) (b : α) => Transfer.ReprMapClass.enc a = b, fwd := { map := Transfer.ReprMapClass.enc }, bwd := { } }