The equivalence bridge + Param weakening

Lifts the relation-hierarchy classes (Transfer/Base/Hierarchy.lean) into the Param (m,n) lattice (ParamHierarchy.lean) and provides the Param-level weakening maps (forget structure in one direction).

A precise observation about ReprEquivClass

ReprEquivClass A α carries enc, enc_inj, a decoder dec : α → A, and the left inverse dec_enc : dec (enc a) = a. With the graph relation R a b := enc a = b:

• forward is map3 (the graph makes both inclusions identities);
• backward is map2b — the decoder dec plus R_in_map (enc a = b → dec b = a, proved from dec_enc). It is not map2a/map3, because that would need the right inverse enc (dec b) = b, which ReprEquivClass does not mandate (only the left inverse). A two-sided bijection would reach map3/map4.

So a left-inverse encoding is exactly a Param map3 map2b — the lattice pins down the asymmetry that the coarse map/embedding/equiv view hides.

def Transfer.Param.paramOfEquiv {A α : Type u} [ReprEquivClass A α] : Param MapClass.map3 MapClass.map2b A α

A left-inverse encoding (ReprEquivClass) as a Param map3 map2b: forward map3 (graph of enc), backward map2b (decoder dec + R_in_map from the left inverse dec_enc).

Equations

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

Param-level weakening (forget in the forward direction)

def Transfer.Param.Param.fwdMap3ToMap2a {n : MapClass} {A B : Type u} (p : Param MapClass.map3 n A B) : Param MapClass.map2a n A B

Forget forward map3 down to map2a.

Equations

• p.fwdMap3ToMap2a = { R := p.R, fwd := Transfer.Param.Map3Has.toMap2a p.fwd, bwd := p.bwd }

def Transfer.Param.Param.fwdMap3ToMap1 {n : MapClass} {A B : Type u} (p : Param MapClass.map3 n A B) : Param MapClass.map1 n A B

Forget forward map3 down to map1.

Equations

• p.fwdMap3ToMap1 = { R := p.R, fwd := (Transfer.Param.Map3Has.toMap2a p.fwd).toMap1, bwd := p.bwd }

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

Forget the backward structure entirely (n → map0).

Equations

• p.bwdToMap0 = { R := p.R, fwd := p.fwd, bwd := { } }