src/Categories_ch1_3.v

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