theory.ua_subvariety

Require Import
  RelationClasses Morphisms Program
  universal_algebra canonical_names ua_subalgebra.


Section contents.
  Context `{InVariety et A} `{@ClosedSubset et A _ _ P}.
  Definition Pvars (vars: Vars et (carrier P) nat): Vars et A nat
    := λ s n, ` (vars s n).


  Program Fixpoint heq {o}: op_type (carrier P) o op_type A o Prop :=
    match o with
    | ne_list.one _ => λ a b, `a = b
    | ne_list.cons _ _ => λ a b, u, heq (a u) (b u)
    end.

  Instance heq_proper: Proper ((=) ==> (=) ==> iff) (@heq o).

  Lemma heq_eval vars {o} (t: T et o): heq (eval et vars t) (eval et (Pvars vars) t).

  Lemma heq_eval_const vars {o} (t: T et (ne_list.one o)): ` (eval et vars t) = eval et (Pvars vars) t.

  Lemma laws s: et_laws et s vars: a, nat carrier P a, eval_stmt et vars s.


  Global Instance: InVariety et (carrier P) := { variety_laws := laws }.

End contents.