categories.JMcat

Require
  JMrelation.
Require Import
  Relation_Definitions abstract_algebra interfaces.functors theory.categories.

Record Object := object
  { obj:> Type
  ; Arrows_inst: Arrows obj
  ; Equiv_inst: x y: obj, Equiv (x y)
  ; CatId_inst: CatId obj
  ; CatComp_inst: CatComp obj
  ; Category_inst: Category obj }.

Implicit Arguments object [[Arrows_inst] [Equiv_inst] [CatId_inst] [CatComp_inst] [Category_inst]].

Record Arrow (x y: Object): Type := arrow
  { map_obj:> obj x obj y
  ; Fmap_inst: Fmap map_obj
  ; Functor_inst: Functor map_obj _ }.

Implicit Arguments arrow [[x] [y]].

Instance: Arrows Object := Arrow.

Section contents.
  Implicit Arguments map_obj [[x] [y]].

  Section more_arrows.
    Context (x y: Object).

    Global Instance e: Equiv (x y) := λ a b,
      ( v, a v b v)
      ( `(f: v w), JMrelation.R (=) (fmap a f) _ (=) (fmap b f)).

    Let e_refl: Reflexive e.

    Let e_sym: Symmetric e.

    Let e_trans: Transitive e.

    Global Instance: Setoid (x y).
  End more_arrows.

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

  Global Program Instance: CatComp Object := λ _ _ _ x y, arrow (x y) _ _.

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

  Global Instance: Category Object.
End contents.