varieties.open_terms

Require Import
  RelationClasses Relation_Definitions List Morphisms
  universal_algebra abstract_algebra canonical_names
  theory.categories categories.varieties.

Section contents.
  Context
    (operation: Set) (operation_type: operation OpType unit).

  Let sig := Build_Signature unit operation operation_type.

  Context (laws: EqEntailment sig Prop).

  Let et := Build_EquationalTheory sig laws.

  Context `{Setoid A}.

  Notation OpenTerm := (Term et A).   Definition OpenTerm0 a := OpenTerm (ne_list.one a).


  Fixpoint app_tree {o}: OpenTerm o op_type OpenTerm0 o :=
    match o with
    | ne_list.one _ => id
    | ne_list.cons _ _ => λ x y, app_tree (App _ _ _ _ x y)
    end.

  Instance: AlgebraOps et OpenTerm0 := λ x, app_tree (Op _ _ x).


  Inductive ee: o, Equiv (OpenTerm o) :=
    | e_vars a a': a = a' Var et A a tt = Var et A a' tt
    | e_refl o: Reflexive (ee o)
    | e_trans o: Transitive (ee o)
    | e_sym o: Symmetric (ee o)
    | e_sub o h: Proper ((=) ==> (=) ==> (=)) (App _ _ h o)
    | e_law (s: EqEntailment et): et_laws et s (v: Vars et OpenTerm0 nat),
      ( x, In x (entailment_premises _ s) eval et v (fst (projT2 x)) = eval et v (snd (projT2 x)))
        eval et v (fst (projT2 (entailment_conclusion _ s))) = eval et v (snd (projT2 (entailment_conclusion _ s))).



  Instance: a, Equiv (OpenTerm0 a) := λ a, ee (ne_list.one a).

  Instance: a, Setoid (OpenTerm0 a).


  Let structural_eq a: relation _ := @op_type_equiv unit OpenTerm0 (λ _, eq) a.

  Instance structural_eq_refl a: Reflexive (structural_eq a).


  Instance app_tree_proper: o, Proper ((=) ==> (=)) (@app_tree o).

  Instance: Algebra et OpenTerm0.


  Lemma laws_hold s (L: et_laws et s): vars, eval_stmt _ vars s.


  Global Instance: InVariety et OpenTerm0.

  Definition the_object: varieties.Object et := varieties.object et OpenTerm0.

End contents.