File OpmlModel

From MatchingLogic.Utils Require Export Surj.
From MatchingLogic.OPML Require Export OpmlSignature.
From stdpp Require Export propset.


Record OPMLModelIsomorphism {Σ : OPMLSignature} (M1 M2 : OPMLModel) := {
    omi_f : (om_unified_carrier M1) → (om_unified_carrier M2) ;
    omi_inj :: Inj (=) (=) omi_f ;
    omi_surj :: Surj' (=) omi_f ;
    omi_app :
        ∀ (s : opml_symbol) (args : list (om_unified_carrier M1)),
        omi_f <$> (@om_app Σ M1 s args) ≡ @om_app Σ M2 s (omi_f <$> args) ;
}.