src/Categories_ch1_3.v

   1 (******************************************************************************)
   2 (* Chapter 1.3: Categories                                                    *)
   3 (******************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8
   9 (* definition 1.1 *)
  10 Class Category
  11 ( Ob               :  Type                    )
  12 ( Hom              :  Ob -> Ob -> Type        ) :=
  13 { hom              := Hom                                                          where "a ~> b" := (hom a b)
  14 ; ob               := Ob
  15
  16 ; id               :  forall  a,                          a~>a
  17 ; comp             :  forall  a b c,                      a~>b -> b~>c -> a~>c     where "f >>> g" := (comp _ _ _ f g)
  18
  19 ; eqv              :  forall  a b,   (a~>b) -> (a~>b) -> Prop                      where "f ~~ g" := (eqv _ _ f g)
  20 ; eqv_equivalence  :  forall  a b,   Equivalence (eqv a b)
  21 ; comp_respects    :  forall  a b c, Proper (eqv a b ==> eqv b c ==> eqv a c) (comp _ _ _)
  22
  23 ; left_identity    :  forall `(f:a~>b),                       id a >>> f  ~~ f
  24 ; right_identity   :  forall `(f:a~>b),                       f  >>> id b ~~ f
  25 ; associativity    :  forall `(f:a~>b)`(g:b~>c)`(h:c~>d), (f >>> g) >>> h ~~ f >>> (g >>> h)
  26 }.
  27 Coercion ob      :      Category >-> Sortclass.
  28
  29 Notation "a ~> b"         := (@hom _ _ _ a b)                      :category_scope.
  30 Notation "f ~~ g"         := (@eqv _ _ _ _ _ f g)                  :category_scope.
  31 Notation "f >>> g"        := (comp _ _ _ f g)                      :category_scope.
  32 Notation "a ~~{ C }~~> b" := (@hom _ _ C a b)       (at level 100) :category_scope.
  33     (* curious: I declared a Reserved Notation at the top of the file, but Coq still complains if I remove "at level 100" *)
  34
  35 Open Scope category_scope.
  36
  37 Hint Extern 3 => apply comp_respects.
  38 Hint Extern 1 => apply left_identity.
  39 Hint Extern 1 => apply right_identity.
  40
  41 Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:Category Ob Hom)(a b:Ob) : (hom a b) (eqv a b)
  42   reflexivity proved by  (@Equivalence_Reflexive  _ _ (eqv_equivalence a b))
  43   symmetry proved by     (@Equivalence_Symmetric  _ _ (eqv_equivalence a b))
  44   transitivity proved by (@Equivalence_Transitive _ _ (eqv_equivalence a b))
  45   as parametric_relation_eqv.
  46   Add Parametric Morphism `(c:Category Ob Hom)(a b c:Ob) : (comp a b c)
  47   with signature (eqv _ _ ==> eqv _ _ ==> eqv _ _) as parametric_morphism_comp.
  48   auto.
  49   Defined.
  50
  51 Hint Constructors Equivalence.
  52 Hint Unfold Reflexive.
  53 Hint Unfold Symmetric.
  54 Hint Unfold Transitive.
  55 Hint Extern 1 (Proper _ _) => unfold Proper; auto.
  56 Hint Extern 1 (Reflexive ?X) => unfold Reflexive; auto.
  57 Hint Extern 1 (Symmetric ?X) => unfold Symmetric; intros; auto.
  58 Hint Extern 1 (Transitive ?X) => unfold Transitive; intros; auto.
  59 Hint Extern 1 (Equivalence ?X) => apply Build_Equivalence.
  60 Hint Extern 8 (respectful _ _ _ _) => unfold respectful; auto.
  61
  62 Hint Extern 4 (?A ~~ ?A) => reflexivity.
  63 Hint Extern 6 (?X ~~ ?Y) => apply Equivalence_Symmetric.
  64 Hint Extern 7 (?X ~~ ?Z) => match goal with [H : ?X ~~ ?Y, H' : ?Y ~~ ?Z |- ?X ~~ ?Z] => transitivity Y end.
  65 Hint Extern 10 (?X >>> ?Y ~~ ?Z >>> ?Q) => apply comp_respects; auto.
  66
  67 (* handy for rewriting *)
  68 Lemma juggle1 : forall `{C:Category}`(f:a~>b)`(g:b~>c)`(h:c~>d)`(k:d~>e), (((f>>>g)>>>h)>>>k) ~~ (f>>>(g>>>h)>>>k).
  69   intros; setoid_rewrite <- associativity; reflexivity.
  70   Defined.
  71 Lemma juggle2 : forall `{C:Category}`(f:a~>b)`(g:b~>c)`(h:c~>d)`(k:d~>e), (f>>>(g>>>(h>>>k))) ~~ (f>>>(g>>>h)>>>k).
  72   intros; repeat setoid_rewrite <- associativity. reflexivity.
  73   Defined.
  74 Lemma juggle3 : forall `{C:Category}`(f:a~>b)`(g:b~>c)`(h:c~>d)`(k:d~>e), ((f>>>g)>>>(h>>>k)) ~~ (f>>>(g>>>h)>>>k).
  75   intros; repeat setoid_rewrite <- associativity. reflexivity.
  76   Defined.
  77
  78
  79
  80
  81