theory.ua_mapped_operations

Require Import
  abstract_algebra universal_algebra.

Section contents.
  Variable Sorts: Set.

  Section map_op.


    Context {A B: Sorts Type}
      `{ a, Equiv (A a)} `{ a, Equiv (B a)}
      (ab: a, A a B a)
      (ba: a, B a A a)
      `{ a, Proper ((=) ==> (=)) (ab a)}
      `{ a, Proper ((=) ==> (=)) (ba a)}.

    Fixpoint map_op {o: OpType Sorts}: op_type A o op_type B o :=
      match o return op_type A o op_type B o with
      | ne_list.one u => ab u
      | ne_list.cons _ _ => λ x y, map_op (x (ba _ y))
      end.

    Global Instance map_op_proper o: Proper ((=) ==> (=)) (@map_op o).

  End map_op.


  Context {A B: Sorts Type} {e: a, Equiv (B a)} `{ b, Equivalence (e b)}
   (ab: a, A a B a) (ba: a, B a A a).

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

   Context `(iso: a (x: B a), ab (ba x) = x).

  Lemma map_iso o (x: op_type B o) (xproper: Proper (=) x):
    map_op ab ba (map_op ba ab x) = x.

End contents.