# 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.