theory.ua_transference

Require Import
  abstract_algebra universal_algebra ua_homomorphisms
  canonical_names theory.categories ua_mapped_operations.

Require categories.varieties.

Section contents.

  Context (et: EquationalTheory) `{InVariety et A} `{InVariety et B}
    `{!HomoMorphism et A B ab} `{!HomoMorphism et B A ba}
    (i: iso_arrows (varieties.arrow et ab) (varieties.arrow et ba)).

  Implicit Arguments ab [[a]].
  Implicit Arguments ba [[a]].

  Let ab_proper a: Proper ((=) ==> (=)) (@ab a).

  Let ba_proper a: Proper ((=) ==> (=)) (@ba a).

  Let epA: V n, Proper ((=) ==> eq ==> (=)) (@eval _ A _ V n) := _.
  Let epB: V n, Proper ((=) ==> eq ==> (=)) (@eval _ B _ V n) := _.

  Let ab_ba: b (a: B b), ab (ba a) = a := proj1 i.
  Let ba_ab: b (a: A b), ba (ab a) = a := proj2 i.

  Program Lemma transfer_eval n (t: Term et nat n) (v: Vars et B nat):
    eval et (A:=A) (λ _ i, ba (v _ i)) t = map_op _ (@ba) (@ab) (eval et v t).

  Program Lemma transfer_eval' n (t: Term et nat n) (v: Vars et B nat):
    map_op _ (@ab) (@ba) (eval et (A:=A) (λ _ i, ba (v _ i)) t) = eval et v t.

  Program Lemma transfer_statement_and_vars (s: Statement et) (v: Vars et B nat):
    eval_stmt et v s eval_stmt et (A:=A) (λ _ i, ba (v _ i)) s.

  Theorem transfer_statement (s: Statement et): ( v, eval_stmt et (A:=A) v s) ( v, eval_stmt et (A:=B) v s).

End contents.