Require Import
  universal_algebra ua_homomorphisms
  theory.categories categories.varieties.
Require theory.setoids.

Section algebras.
    (sig: Signature) (I: Type) (carriers: I sorts sig Type)
    `( i s, Equiv (carriers i s))
    `{ i, AlgebraOps sig (carriers i)}
    `{ i, Algebra sig (carriers i)}.

  Definition carrier: sorts sig Type := λ sort, i: I, carriers i sort.

  Fixpoint rec_impl o: ( i, op_type (carriers i) o) op_type carrier o :=
    match o return ( i, op_type (carriers i) o) op_type carrier o with
    | _ => id
    | ne_list.cons _ g => λ X X0, rec_impl g (λ i, X i (X0 i))

  Let u (s: sorts sig): Equiv (forall i : I, carriers i s).

  Instance rec_impl_proper: o,
    Proper (@setoids.product_equiv I _ (fun _ => op_type_equiv _ _ _) ==> (=)) (rec_impl o).

  Global Instance product_ops: AlgebraOps sig carrier := λ o, rec_impl (sig o) (λ i, algebra_op o).

  Instance: o: sig, Proper (=) (algebra_op o: op_type carrier (sig o)).

  Instance product_e sort: Equiv (carrier sort) := (=).
  Global Instance product_algebra: Algebra sig carrier := {}.

  Lemma preservation i o: Preservation sig carrier (carriers i) (λ _ v, v i) (algebra_op o) (algebra_op o).

  Lemma algebra_projection_morphisms i: @HomoMorphism sig carrier (carriers i) _ _ _ _ (λ a v, v i).

End algebras.

Section varieties.
    (et: EquationalTheory)
    (I: Type) (carriers: I sorts et Type)
    `( i s, Equiv (carriers i s))
    `( i, AlgebraOps et (carriers i))
    `( i, InVariety et (carriers i)).

  Typeclasses Transparent Equiv.

  Notation carrier := (carrier et I carriers).
  Let carrier_e := product_e et I carriers _.

  Fixpoint nqe {t}: op_type carrier t ( i, op_type (carriers i) t) Prop :=
   match t with
   | _ => λ f g, i, f i = g i
   | ne_list.cons _ _ => λ f g, tuple, nqe (f tuple) (λ i, g i (tuple i))
  Instance nqe_proper t: Proper ((=) ==> (λ x y, i, x i = y i) ==> iff) (@nqe t).

  Lemma nqe_always {t} (term: Term _ nat t) vars:
    nqe (eval et vars term) (λ i, eval et (λ sort n, vars sort n i) term).

  Lemma component_equality_to_product t
    (A A': op_type carrier t)
    (B B': i, op_type (carriers i) t):
    ( i, B i = B' i) nqe A B nqe A' B' A = A'.

  Lemma laws_hold s: et_laws et s vars, eval_stmt et vars s.

  Global Instance product_variety: InVariety et carrier (e:=carrier_e).

End varieties.

Require categories.varieties.

Section categorical.

    (et: EquationalTheory).

  Global Instance: Producer (varieties.Object et) := λ I carriers,
    {| varieties.variety_carriers := λ s, i, carriers i s
    ; varieties.variety_proof := product_variety et I _ _ _ (fun H => varieties.variety_proof et (carriers H)) |}.

  Section for_a_given_c.
  Context (I: Type) (c: I varieties.Object et).

  Global Program Instance: ElimProduct c (product c) := λ i _ c, c i.

  Global Program Instance: IntroProduct c (product c) := λ _ h a X i, h i a X.

  Global Instance: Product c (product c).

  End for_a_given_c.

  Global Instance: HasProducts (varieties.Object et) := {}.

End categorical.