structure ISAR.Dialect : Type 1

An abstract Dialect represents a semantic view over the representation-free substrate. For a given dialect, we have:

1. Object: The type of dialect objects/terms.
2. Obs: The type of observations or results of evaluation.
3. ObsEq: The observational equivalence relation on observations.
4. eval: The dialect's evaluation function.
5. encode: A compiler/encoder mapping dialect objects to substrate terms (ISKSubtype).
6. decode: A decoder mapping substrate quotient classes (InvariantLayer) to observations.
7. preserves: The main coherence/preservation law, showing that decoding the quotient class of an encoded object is observationally equivalent to evaluating the object in the dialect.

• Object : Type
• Obs : Type
• ObsEq : self.Obs → self.Obs → Prop
• is_equiv : Equivalence self.ObsEq
• eval : self.Object → self.Obs
• encode : self.Object → ISKSubtype
• decode : InvariantLayer → self.Obs
• preserves (x : self.Object) : self.ObsEq (self.decode ⟦self.encode x⟧) (self.eval x)

def ISAR.Dialect.setoid (D : Dialect) : Setoid D.Obs

The equivalence relation setoid on a Dialect's observations.

Equations

• D.setoid = { r := D.ObsEq, iseqv := ⋯ }