Require Import
  List abstract_algebra.

Local Notation ne_list := ne_list.L.

Section with_sorts.
  Variable Sorts: Set.

  Definition OpType := ne_list Sorts.

  Definition result: OpType Sorts := @ne_list.last _.

  Variable carrier: Sorts Type.

  Fixpoint op_type (o: OpType): Type :=
    match o with
    | a => carrier a
    | ne_list.cons a g => carrier a op_type g

  Context `{e: s, Equiv (carrier s)}.

  Fixpoint op_type_equiv o: Equiv (op_type o) :=
    match o with
    | _ => _: Equiv (carrier _)
    | ne_list.cons A g => (e A ==> op_type_equiv g)%signature

  Global Instance sig_type_sym `{ s, Symmetric (e s)}: Symmetric (op_type_equiv o).

  Global Instance sig_type_trans `{ s, Reflexive (e s)} `{ s, Transitive (e s)}: Transitive (op_type_equiv o).

  Hint Unfold op_type.

  Global Instance sig_type_trans' `{ s, Symmetric (e s)} `{ s, Transitive (e s)}: Transitive (op_type_equiv o).

  Lemma sig_type_refl `{ a, Reflexive (e a)} (o: OpType) a (x: op_type (ne_list.cons a o)) y:
    Proper (=) x op_type_equiv o (x y) (x y).

End with_sorts.

Implicit Arguments op_type [[Sorts]].

Hint Extern 0 (Equiv (op_type _ _ )) => eapply @op_type_equiv : typeclass_instances.

Inductive Signature: Type :=
  { sorts: Set
  ; operation:> Set
  ; operation_type:> operation OpType sorts }.

Definition single_sorted_signature {Op: Set} (arities: Op nat): Signature :=
  Build_Signature unit Op (ne_list.replicate_Sn tt arities).

Class AlgebraOps (σ: Signature) (A: sorts Type) := algebra_op: o, op_type A ( o).

Class Algebra
  (σ: Signature)
  (carriers: sorts Type)
  {e: a, Equiv (carriers a)}
  `{AlgebraOps carriers}: Prop :=
    { algebra_setoids:> a, Setoid (carriers a)
    ; algebra_propers:> o: , Proper (=) (algebra_op o) }.