categories.categories

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]].
Hint Extern 0 (Equiv (_ _)) => eapply @Equiv_inst : typeclass_instances.


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 Program Instance e: Equiv (x y) := λ a b,
      exists X: _, isoT _ _, (p q: x) (r: p q),
       fmap a r snd (X p) = snd (X q) fmap b r.

    Let e_refl: Reflexive e.

    Program Let sym_arrows (a b: x y) (v: x) (p: isoT (a v) (b v)): isoT (b v) (a v)
        := (snd p, fst p).


    Let e_sym: Symmetric e.

    Program Let trans_arrows (x0 y0 z: x y) (v: x)
     (x1: sig (λ (p: (x0 v y0 v) * _), uncurry iso_arrows p))
     (x2: sig (λ (p: (y0 v z v) * _), uncurry iso_arrows p)):
      isoT (x0 v) (z v) := (fst x2 fst x1, snd x1 snd x2).


    Let e_trans: Transitive e.

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

  Let obj_iso (x: Object): Equiv x := @iso x _ _ _ _.

  Typeclasses Transparent Arrows.
  Global Instance: (x y: Object) (a: x y), Setoid_Morphism (map_obj a).

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

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

  Program Let proper_arrows (x y z: Object) (x0 y0: y z) (x1 y1: x y)
    (f: v, @isoT _ _ _ _ _ (map_obj x0 v) (map_obj y0 v))
    (g: v, @isoT _ _ _ _ _ (map_obj x1 v) (map_obj y1 v)) (v: x):
      @isoT _ _ _ _ _ (map_obj x0 (map_obj x1 v)) (map_obj y0 (map_obj y1 v))
   := (fst (f (y1 v)) fmap x0 (fst (g v)), fmap x0 (snd (g v)) snd (f (y1 v))).


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

  Program Let id_lr_arrows (x y: Object) (a: y x) v: isoT (map_obj a v) (map_obj a v)
    := (cat_id, cat_id).


  Instance: forall x y: Object, LeftIdentity (comp x _ y) cat_id.

  Instance: forall x y: Object, RightIdentity (comp x _ y) cat_id.

  Section associativity.
    Variables (w x y z: Object) (a: w x) (b: x y) (c: y z).

    Program Definition associativity_arrows (v: w): isoT (c (b (a v))) (c (b (a v))) :=
      (fmap c (fmap b (fmap a cat_id)), fmap c (fmap b (fmap a cat_id))).
  End associativity.

  Instance: ArrowsAssociative Object.

  Global Instance: Category Object := {}.
End contents.