Category.v

Require Import Coq.Logic.ProofIrrelevance.
Require Import Coq.Program.Tactics.

Ltac simpl_exist_eq :=
  match goal with
  | [ |- exist _ ?x _ = exist _ ?y _]
    => let H := fresh "H"
       in cut (x = y);
          [ intro H;
            apply eq_sig with (p:=H);
            apply proof_irrelevance
          | (* nothing *)
          ]
  end.

(** * Basic Constructions

    ** Categories

    *** Definition
 *)

Class category
      {object:  Type}
      (arrow:   object -> object -> Type)
  := { comp {c b a:  object}
       : arrow b c -> arrow a b -> arrow a c
     ; id (a:  object)
       : arrow a a
     ; comp_assoc_law {d c b a:  object}
                      (h:        arrow c d)
                      (g:        arrow b c)
                      (f:        arrow a b)
       : comp (comp h g) f = comp h (comp g f)
     ; id_assoc_1_law {b a:  object}
                      (f:  arrow a b)
       : comp (id b) f = f
     ; id_assoc_2_law {b a:  object}
                      (f:  arrow a b)
       : comp f (id a) = f
     }.

Arguments category       [object] (arrow).
Arguments comp           [object arrow _ c b a] (_ _).
Arguments id             [object arrow _] (a).
Arguments comp_assoc_law [object arrow _ d c b a] (h g f).
Arguments id_assoc_1_law [object arrow _ b a] (f).
Arguments id_assoc_2_law [object arrow _ b a] (f).

Notation "f <<< g" := (comp f g) (at level 50).
Notation "g >>> f" := (f <<< g) (at level 50).

(** *** Example: the Set Category *)

Module SET.
  Definition func := fun a b => a -> b.

  Definition comp
             {c b a: Type}
             (g: func b c)
             (f: func a b)
    : func a c :=
    fun x => g (f x).

  Definition id
             (a:  Type)
    : func a a :=
     fun x => x.

  Lemma comp_assoc_law
    : forall {d c b a: Type}
             (h: func c d)
             (g: func b c)
             (f: func a b),
    comp (comp h g) f
    = comp h (comp g f).
  Proof.
    reflexivity.
  Qed.

  Lemma id_assoc_1_law
    : forall {b a: Type}
             (f:  func a b),
      comp (id b) f = f.
  Proof.
    reflexivity.
  Qed.

  Lemma id_assoc_2_law
    : forall {b a: Type}
             (f:  func a b),
      comp f (id a) = f.
  Proof.
    reflexivity.
  Qed.

  Instance set_category
    : category func :=
    { comp           := @comp
    ; id             := id
    ; comp_assoc_law := @comp_assoc_law
    ; id_assoc_1_law := @id_assoc_1_law
    ; id_assoc_2_law := @id_assoc_2_law
    }.
End SET.

(** *** Example: The 0 Category *)

Module O.
  Inductive empty := .
  Variable arrow : empty -> empty -> Type.

  Definition comp
             {c b a: empty}
             (g: arrow b c)
             (f: arrow a b)
    : arrow a c.
    inversion a.
  Defined.

  Definition id
             (a: empty)
    : arrow a a.
    inversion a.
  Defined.

  Lemma comp_assoc_law
    : forall {d c b a: empty}
             (h: arrow c d)
             (g: arrow b c)
             (f: arrow a b),
    comp (comp h g) f
    = comp h (comp g f).
  Proof.
    inversion a.
  Qed.

  Lemma id_assoc_1_law
    : forall {b a: empty}
             (f:  arrow a b),
      comp (id b) f = f.
  Proof.
    inversion a.
  Qed.

  Lemma id_assoc_2_law
    : forall {b a: empty}
             (f:  arrow a b),
      comp f (id a) = f.
  Proof.
    inversion a.
  Qed.

  Instance empty_category
    : category arrow :=
    { comp           := @comp
    ; id             := id
    ; comp_assoc_law := @comp_assoc_law
    ; id_assoc_1_law := @id_assoc_1_law
    ; id_assoc_2_law := @id_assoc_2_law
    }.
End O.

(** *** Example: Mon **)
Class monoid
      {a:   Type}
      (op:  a -> a -> a)
      (e:   a) :=
  { op_assoc (x y z:  a)
    : op (op x y) z = op x (op y z)
  ; e_neutral_1_law (x:  a)
    : op x e = e
  ; e_neutral_2_law (x:  a)
    : op e x = e
  }.

Section Homomorph.
  Variables (a b:   Type)
            (op_a:  a -> a -> a)
            (e_a:   a)
            (op_b:  b -> b -> b)
            (e_b:   b).

  Definition homomorphism
            `{monoid a op_a e_a}
            `{monoid b op_b e_b}
    := { f:  a -> b | f e_a = e_b /\ forall (x y:  a), f (op_a x y) = op_b (f x) (f y) }.
End Homomorph.

Arguments homomorphism (a b) [op_a e_a op_b e_b _ _].

Module Mon.
  Record Monoid :=
    { set: Type
    ; op: set -> set -> set
    ; e:  set
    ; monoid_instance :> monoid  op e
    }.

  Definition Homomorphism
             (a b:  Monoid)
    := homomorphism (H := monoid_instance a)
                    (H0 := monoid_instance b)
                    (set a)
                    (set b).

  Program Definition comp
          {c b a:  Monoid}
          (g:      Homomorphism b c)
          (f:      Homomorphism a b)
    : Homomorphism a c :=
    fun x => g (f x).
  Next Obligation.
    induction f as [f [Hf_e Hf_op]].
    induction g as [g [Hg_e Hg_op]].
    cbn in *.
    split.
    + now (rewrite Hf_e; rewrite Hg_e).
    + intros x y.
      now (rewrite Hf_op; rewrite Hg_op).
  Defined.

  Program Definition id
          (a:  Monoid)
    : Homomorphism a a :=
    fun x => x.

  Lemma comp_assoc_law
    : forall {d c b a: Monoid}
             (h: Homomorphism c d)
             (g: Homomorphism b c)
             (f: Homomorphism a b),
      comp (comp h g) f
      = comp h (comp g f).
  Proof.
    intros d c b a [h [Hh_e Hh_op]] [g [Hg_e Hg_op]] [f [Hf_e Hf_op]].
    unfold comp in *.
    cbn in *.
    simpl_exist_eq.
    reflexivity.
  Qed.

  Lemma id_assoc_1_law
    : forall {b a: Monoid}
             (f:  Homomorphism a b),
      comp (id b) f = f.
  Proof.
    intros b a [f [Hf_e Hf_op]].
    unfold comp, id in *.
    cbn in *.
    simpl_exist_eq.
    now repeat rewrite id_assoc_1_law.
  Qed.

  Lemma id_assoc_2_law
    : forall {b a: Monoid}
             (f:  Homomorphism a b),
      comp f (id a) = f.
  Proof.
    intros b a [f [Hf_e Hf_op]].
    unfold comp, id in *.
    cbn in *.
    simpl_exist_eq.
    now repeat rewrite id_assoc_2_law.
  Qed.

  Instance mon_category
    : category Homomorphism :=
    { comp           := @comp
    ; id             := id
    ; comp_assoc_law := @comp_assoc_law
    ; id_assoc_1_law := @id_assoc_1_law
    ; id_assoc_2_law := @id_assoc_2_law
    }.
End Mon.

(** *** Example: The Cat→ Category *)

Module CatArrow.
  Variables (object:  Type)
            (arrow:   object -> object -> Type).

  Record cat_arrow_object :=
    { dom: object
    ; cod: object
    ; fn:  arrow dom cod
    }.

  Definition cat_arrow_arrow
            `{category object arrow}
             (f f': cat_arrow_object) :=
    { o | comp (fn f') (fst o) = comp (snd o) (fn f)}.

  Program Definition comp
            `{category object arrow}
             {c b a: cat_arrow_object}
             (g:     cat_arrow_arrow b c)
             (f:     cat_arrow_arrow a b)
    : cat_arrow_arrow a c :=
    (comp (fst g) (fst f), comp (snd g) (snd f)).
  Next Obligation.
    induction f as [(x,y) Hf]; induction g as [(x',y') Hg].
    cbn in *.
    rewrite <- (comp_assoc_law (fn c) _ _).
    rewrite Hg.
    rewrite (comp_assoc_law y' _ _).
    rewrite Hf.
    rewrite <- (comp_assoc_law y' _ _).
    reflexivity.
  Defined.

  Program Definition id
         `{category object arrow}
          (a:  cat_arrow_object)
    : cat_arrow_arrow a a :=
    (id (dom a), id (cod a)).
  Next Obligation.
    rewrite id_assoc_1_law.
    rewrite id_assoc_2_law.
    reflexivity.
  Defined.

  Lemma comp_assoc_law
       `{category object arrow}
    : forall {d c b a: cat_arrow_object}
             (h: cat_arrow_arrow c d)
             (g: cat_arrow_arrow b c)
             (f: cat_arrow_arrow a b),
      comp (comp h g) f
      = comp h (comp g f).
  Proof.
    intros [A B f] [A' B' f'] [A'' B'' f''] [A''' B''' f''']
           [(x,y) Hh] [(x',y') Hg] [(x'',y'') Hf].
    unfold comp.
    cbn in *.
    simpl_exist_eq.
    now repeat rewrite comp_assoc_law.
  Qed.

  Lemma id_assoc_1_law
       `{category object arrow}
    : forall {b a: cat_arrow_object}
             (f:  cat_arrow_arrow a b),
      comp (id b) f = f.
  Proof.
    intros [A B f] [A' B' f'] [(a,b) G].
    cbn.
    unfold comp, id in *.
    cbn in *.
    simpl_exist_eq.
    now repeat rewrite id_assoc_1_law.
  Qed.

  Lemma id_assoc_2_law
       `{category object arrow}
    : forall {b a: cat_arrow_object}
             (f:  cat_arrow_arrow a b),
      comp f (id a) = f.
  Proof.
    intros [A B f] [A' B' f'] [(a,b) G].
    cbn.
    unfold comp, id in *.
    cbn in *.
    simpl_exist_eq.
    now repeat rewrite id_assoc_2_law.
  Qed.

  Instance cat_arrow_category
          `{H: category object arrow}
    : category cat_arrow_arrow :=
    { comp           := @comp H
    ; id             := id
    ; comp_assoc_law := @comp_assoc_law H
    ; id_assoc_1_law := @id_assoc_1_law H
    ; id_assoc_2_law := @id_assoc_2_law H
    }.
End CatArrow.

Section Morphism.
  Variables (object:  Type)
            (arrow:   object -> object -> Type).

  Definition monomorphism
            `{category object arrow}
             {c b:  object}
             (f:    arrow b c)
    := forall {a:  object}
              (g h:   arrow a b),
       g >>> f = h >>> f -> g = h.

  Definition epimorphism
            `{category object arrow}
             {c b:  object}
             (f:    arrow b c)
    := forall {a:  object}
              (g h:   arrow c a),
       f >>> g = f >>> h -> g = h.
End Morphism.

Arguments monomorphism [object arrow H c b] (f).
Arguments epimorphism [object arrow H c b] (f).