categories.setoids

Require Import
  Relation_Definitions abstract_algebra theory.categories.

Inductive Object := object { T:> Type; e: Equiv T; setoid_proof: Setoid T }.


Section contents.
  Global Instance: Arrows Object := λ A B, sig (@Setoid_Morphism A B _ _).

  Global Program Instance: x y: Object, Equiv (x y) := λ _ _, respectful (=) (=).

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

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

  Local Obligation Tactic := idtac.
  Global Program Instance: CatComp Object := λ _ _ _, compose.

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

  Global Instance: Category Object.

  Global Instance: Producer Object := λ _ c, object ( i, c i) (λ x y, i, x i = y i) _.

  Section product.
    Context {Index: Type} (c: Index Object).

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

    Global Program Instance: IntroProduct c (product c) := λ d df x y, df y x.

    Global Instance: Product c (product c).
  End product.

  Global Instance: HasProducts Object := {}.

  Global Instance mono (X Y: Object) (a: X Y): Injective (` a) Mono a.
End contents.