1 Generalizable All Variables.
2 Require Import Notations.
3 Require Import Categories_ch1_3.
5 (******************************************************************************)
6 (* Chapter 1.4: Functors *)
7 (******************************************************************************)
12 ( fobj : c1 -> c2 ) :=
13 { functor_fobj := fobj
14 ; fmor : forall {a b}, a~>b -> (fobj a)~>(fobj b)
15 ; fmor_respects : forall a b (f f':a~>b), f~~f' -> fmor f ~~ fmor f'
16 ; fmor_preserves_id : forall a, fmor (id a) ~~ id (fobj a)
17 ; fmor_preserves_comp : forall `(f:a~>b)`(g:b~>c), (fmor f) >>> (fmor g) ~~ fmor (f >>> g)
19 (* register "fmor" so we can rewrite through it *)
20 Implicit Arguments fmor [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
21 Implicit Arguments fmor_respects [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
22 Implicit Arguments fmor_preserves_id [ Ob Hom Ob0 Hom0 c1 c2 fobj ].
23 Implicit Arguments fmor_preserves_comp [ Ob Hom Ob0 Hom0 c1 c2 fobj a b c ].
24 Notation "F \ f" := (fmor F f) : category_scope.
25 Add Parametric Morphism `(C1:Category)`(C2:Category)
27 (F:Functor C1 C2 Fobj)
29 : (@fmor _ _ C1 _ _ C2 Fobj F a b)
30 with signature ((@eqv C1 _ C1 a b) ==> (@eqv C2 _ C2 (Fobj a) (Fobj b))) as parametric_morphism_fmor'.
31 intros; apply (@fmor_respects _ _ C1 _ _ C2 Fobj F a b x y); auto.
33 Coercion functor_fobj : Functor >-> Funclass.
35 (* the identity functor *)
36 Definition functor_id `(C:Category) : Functor C C (fun x => x).
37 intros; apply (Build_Functor _ _ C _ _ C (fun x => x) (fun a b f => f)); intros; auto; reflexivity.
40 (* the constant functor *)
41 Definition functor_const `(C:Category) `{D:Category} (d:D) : Functor C D (fun _ => d).
42 apply Build_Functor with (fmor := fun _ _ _ => id d).
48 (* functors compose *)
49 Definition functor_comp
53 `(F:@Functor _ _ C1 _ _ C2 Fobj)`(G:@Functor _ _ C2 _ _ C3 Gobj) : Functor C1 C3 (Gobj ○ Fobj).
54 intros. apply (Build_Functor _ _ _ _ _ _ _ (fun a b m => G\(F\m)));
55 [ abstract (intros; setoid_rewrite H ; auto; reflexivity)
56 | abstract (intros; repeat setoid_rewrite fmor_preserves_id; auto; reflexivity)
57 | abstract (intros; repeat setoid_rewrite fmor_preserves_comp; auto; reflexivity)
60 Notation "f >>>> g" := (@functor_comp _ _ _ _ _ _ _ _ _ _ f _ g) : category_scope.
62 Lemma functor_comp_assoc `{C':Category}`{D:Category}`{E:Category}`{F:Category}
63 {F1obj}(F1:Functor C' D F1obj)
64 {F2obj}(F2:Functor D E F2obj)
65 {F3obj}(F3:Functor E F F3obj)
67 ((F1 >>>> F2) >>>> F3) \ f ~~ (F1 >>>> (F2 >>>> F3)) \ f.
72 (* this is like JMEq, but for the particular case of ~~; note it does not require any axioms! *)
73 Inductive heq_morphisms `{c:Category}{a b:c}(f:a~>b) : forall {a' b':c}, a'~>b' -> Prop :=
74 | heq_morphisms_intro : forall {f':a~>b}, eqv _ _ f f' -> @heq_morphisms _ _ c a b f a b f'.
75 Definition heq_morphisms_refl : forall `{c:Category} a b f, @heq_morphisms _ _ c a b f a b f.
76 intros; apply heq_morphisms_intro; reflexivity.
78 Definition heq_morphisms_symm : forall `{c:Category} a b f a' b' f', @heq_morphisms _ _ c a b f a' b' f' -> @heq_morphisms _ _ c a' b' f' a b f.
79 refine(fun ob hom c a b f a' b' f' isd =>
81 | heq_morphisms_intro f''' z => @heq_morphisms_intro _ _ c _ _ f''' f _
84 Definition heq_morphisms_tran : forall `{C:Category} a b f a' b' f' a'' b'' f'',
85 @heq_morphisms _ _ C a b f a' b' f' ->
86 @heq_morphisms _ _ C a' b' f' a'' b'' f'' ->
87 @heq_morphisms _ _ C a b f a'' b'' f''.
90 apply heq_morphisms_intro.
96 Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:Category Ob Hom)(a b:Ob) : (hom a b) (eqv a b)
97 reflexivity proved by heq_morphisms_refl
98 symmetry proved by heq_morphisms_symm
99 transitivity proved by heq_morphisms_tran
100 as parametric_relation_heq_morphisms.
101 Add Parametric Morphism `(c:Category Ob Hom)(a b c:Ob) : (comp a b c)
102 with signature (eqv _ _ ==> eqv _ _ ==> eqv _ _) as parametric_morphism_comp.
106 Implicit Arguments heq_morphisms [Ob Hom c a b a' b'].
107 Hint Constructors heq_morphisms.
109 Definition EqualFunctors `{C1:Category}`{C2:Category}{F1obj}(F1:Functor C1 C2 F1obj){F2obj}(F2:Functor C1 C2 F2obj) :=
110 forall a b (f f':a~~{C1}~~>b), f~~f' -> heq_morphisms (F1 \ f) (F2 \ f').
111 Notation "f ~~~~ g" := (EqualFunctors f g) (at level 45).
113 Class IsomorphicCategories `(C:Category)`(D:Category) :=
116 ; ic_f : Functor C D ic_f_obj
117 ; ic_g : Functor D C ic_g_obj
118 ; ic_forward : ic_f >>>> ic_g ~~~~ functor_id C
119 ; ic_backward : ic_g >>>> ic_f ~~~~ functor_id D
122 (* this causes Coq to die: *)
123 (* Definition IsomorphicCategories := Isomorphic (CategoryOfCategories). *)