1 (******************************************************************************)
2 (* Chapter 1.3: Categories *)
3 (******************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
12 ( Hom : Ob -> Ob -> Type ) :=
13 { hom := Hom where "a ~> b" := (hom a b)
17 ; comp : forall a b c, a~>b -> b~>c -> a~>c where "f >>> g" := (comp _ _ _ f g)
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 _ _ _)
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)
27 Coercion ob : Category >-> Sortclass.
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" *)
35 Open Scope category_scope.
37 Hint Extern 3 => apply comp_respects.
38 Hint Extern 1 => apply left_identity.
39 Hint Extern 1 => apply right_identity.
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.
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.
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.
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.
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.
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.