The relation hierarchy as classes

Trocq keeps a hierarchy of relation structures and picks, per subterm, the weakest level a transfer needs. This module promotes the ReprTransfer structures into a univalence-free class hierarchy:

ReprMapClass (a map, transfers = forward) ⊂ ReprEmbeddingClass (+ injective, reflects =, so transfers = both ways) ⊂ ReprEquivClass (a bijection — the top level the SIP/univalence route needs).

The hierarchy bottoms out below equivalence: the crypto encodings are embeddings (point/Fp¹²/word serializations are injective, not surjective), so the equality-transfer level is ReprEmbeddingClass, and the layer never requires — nor incurs the TCB cost of — univalence. The per-operation realizations (BinOpRealization / EndoOpRealization / BinOpHomOn in ReprTransfer) are the op-level instances built over these levels; the repr registry (Transfer.Base.Core) indexes them.

class Transfer.ReprMapClass (A α : Type u) : Type u

Level 0: a representation map A → α. Transfers an equality forward (a = a' → enc a = enc a').

• enc : A → α

  The encoding.

class Transfer.ReprEmbeddingClass (A α : Type u) extends Transfer.ReprMapClass A α : Type u

Level 1: a representation embedding — a map that reflects equality (injective). Transfers a decidable equality in both directions.

• enc : A → α
• enc_inj : Function.Injective ReprMapClass.enc

  The encoding reflects equality.

theorem Transfer.ReprEmbeddingClass.eq_iff {A α : Type u} [ReprEmbeddingClass A α] (a a' : A) : ReprMapClass.enc a = ReprMapClass.enc a' ↔ a = a'

Equality transfers across an embedding (both directions).

class Transfer.ReprEquivClass (A α : Type u) extends Transfer.ReprEmbeddingClass A α : Type u

Level 2 (top): a representation equivalence — a bijective encoding. The level the univalence / structure-identity route requires; the crypto encodings do not reach it (they are embeddings, not bijections), which is why the transfer layer stays univalence-free.

• enc : A → α
• enc_inj : Function.Injective ReprMapClass.enc
• dec : α → A

  The inverse decoding.

• dec_enc (a : A) : dec (ReprMapClass.enc a) = a

  dec is a left inverse of enc (hence enc is a bijection onto its range with dec; with enc_inj this is an equivalence on the image).

@[reducible]

def Transfer.endoOpRealizationToEmbeddingClass {A α : Type u} {op : A → A → A} {bop : α → α → α} (R : ReprTransfer.EndoOpRealization op bop) : ReprEmbeddingClass A α

An EndoOpRealization (from ReprTransfer) supplies an embedding level: its enc/enc_inj are exactly a ReprEmbeddingClass. Bridges the op-level realizations to the relation hierarchy.

Equations

• Transfer.endoOpRealizationToEmbeddingClass R = { enc := R.enc, enc_inj := ⋯ }