categories.varieties

Require Import
  abstract_algebra universal_algebra ua_homomorphisms.

Record Object (et: EquationalTheory) : Type := object
  { variety_carriers:> sorts et Type
  ; variety_equiv: a, Equiv (variety_carriers a)
  ; variety_ops: AlgebraOps et variety_carriers
  ; variety_proof: InVariety et variety_carriers }.

Implicit Arguments object [[variety_equiv] [variety_ops] [variety_proof]].

Hint Extern 0 (Equiv (variety_carriers _ _ _)) => eapply @variety_equiv : typeclass_instances.

Section contents.
  Variable et: EquationalTheory.

  Global Instance: Arrows (Object et) := λ X Y, sig (HomoMorphism et X Y).

  Program Definition arrow `{InVariety et A} `{InVariety et B}
    f `{!HomoMorphism et A B f}: object et A object et B := f.

  Global Program Instance: CatId (Object et) := λ _ _, id.

  Global Program Instance: CatComp (Object et) := λ _ _ _ f g v, f v g v.

  Global Program Instance: (x y: Object et), Equiv (x y)
    := λ _ _ x y, b, pointwise_relation _ (=) (x b) (y b).

  Global Instance: (x y: Object et), Setoid (x y).

  Instance: (x y z: Object et), Proper ((=) ==> (=) ==> (=)) (comp x y z).

  Global Instance: Category (Object et).
End contents.