varieties.closed_terms

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

Section contents.
  Variable et: EquationalTheory.


  Let ClosedTerm := (Term et False).
  Let ClosedTerm0 a := ClosedTerm (ne_list.one a).


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

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


  Inductive e: o, Equiv (ClosedTerm o) :=
    | e_refl o: Reflexive (e o)
    | e_trans o: Transitive (e o)
    | e_sym o: Symmetric (e o)
    | e_sub o h: Proper ((=) ==> (=) ==> (=)) (App _ _ h o)
    | e_law (s: EqEntailment et): et_laws et s (v: Vars et ClosedTerm0 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 (ClosedTerm0 a) := λ a, e (ne_list.one a).

  Instance: a, Setoid (ClosedTerm0 a) := {}.


  Let structural_eq a: relation _ := @op_type_equiv (sorts et) ClosedTerm0 (λ _, eq) a.

  Instance structural_eq_refl a: Reflexive (structural_eq a).


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

  Instance: Algebra et ClosedTerm0.


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


  Global Instance: InVariety et ClosedTerm0.


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



  Section for_another_object.
    Variable other: varieties.Object et.


    Definition eval_in_other {o}: ClosedTerm o op_type other o := @eval et other _ False o (no_vars _ other).

    Definition morph a: the_object a other a := eval_in_other.


    Lemma subst_eval o V (v: Vars _ ClosedTerm0 _) (t: Term _ V o):
      @eval _ other _ _ _ (λ x y, eval_in_other (v x y)) t =
      eval_in_other (close _ v t).


    Lemma eval_is_close V x v (t: Term0 et V x): eval et v t close _ v t.


    Instance prep_proper: Proper ((=) ==> (=)) (@eval_in_other o).

    Instance: a, Setoid_Morphism (@eval_in_other (ne_list.one a)).


    Instance: @HomoMorphism et ClosedTerm0 other _ (varieties.variety_equiv et other) _ _ (λ _, eval_in_other).

    Program Definition the_arrow: the_object other := λ _, eval_in_other.


    Theorem arrow_unique: y, the_arrow = y.

  End for_another_object.

  Hint Extern 4 (InitialArrow the_object) => exact the_arrow: typeclass_instances.

  Instance: Initial the_object.


End contents.