1 Generalizable All Variables.
2 Require Import Preamble.
3 Require Import General.
4 Require Import Categories_ch1_3.
6 (******************************************************************************)
7 (* Chapter 1.4: Functors *)
8 (******************************************************************************)
13 ( fobj : c1 -> c2 ) :=
14 { functor_fobj := fobj
15 ; fmor : forall {a b}, a~>b -> (fobj a)~>(fobj b)
16 ; fmor_respects : forall a b (f f':a~>b), f~~f' -> fmor f ~~ fmor f'
17 ; fmor_preserves_id : forall a, fmor (id a) ~~ id (fobj a)
18 ; fmor_preserves_comp : forall `(f:a~>b)`(g:b~>c), (fmor f) >>> (fmor g) ~~ fmor (f >>> g)
20 (* register "fmor" so we can rewrite through it *)
21 Implicit Arguments fmor [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
22 Implicit Arguments fmor_respects [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
23 Implicit Arguments fmor_preserves_id [ Ob Hom Ob0 Hom0 c1 c2 fobj ].
24 Implicit Arguments fmor_preserves_comp [ Ob Hom Ob0 Hom0 c1 c2 fobj a b c ].
25 Notation "F \ f" := (fmor F f) : category_scope.
26 Add Parametric Morphism `(C1:Category)`(C2:Category)
28 (F:Functor C1 C2 Fobj)
30 : (@fmor _ _ C1 _ _ C2 Fobj F a b)
31 with signature ((@eqv C1 _ C1 a b) ==> (@eqv C2 _ C2 (Fobj a) (Fobj b))) as parametric_morphism_fmor'.
32 intros; apply (@fmor_respects _ _ C1 _ _ C2 Fobj F a b x y); auto.
34 Coercion functor_fobj : Functor >-> Funclass.
36 (* the identity functor *)
37 Definition functor_id `(C:Category) : Functor C C (fun x => x).
38 intros; apply (Build_Functor _ _ C _ _ C (fun x => x) (fun a b f => f)); intros; auto; reflexivity.
41 (* the constant functor *)
42 Definition functor_const `(C:Category) `{D:Category} (d:D) : Functor C D (fun _ => d).
43 apply Build_Functor with (fmor := fun _ _ _ => id d).
49 (* functors compose *)
50 Definition functor_comp
54 `(F:@Functor _ _ C1 _ _ C2 Fobj)`(G:@Functor _ _ C2 _ _ C3 Gobj) : Functor C1 C3 (Gobj ○ Fobj).
55 intros. apply (Build_Functor _ _ _ _ _ _ _ (fun a b m => G\(F\m)));
56 [ abstract (intros; setoid_rewrite H ; auto; reflexivity)
57 | abstract (intros; repeat setoid_rewrite fmor_preserves_id; auto; reflexivity)
58 | abstract (intros; repeat setoid_rewrite fmor_preserves_comp; auto; reflexivity)
61 Notation "f >>>> g" := (@functor_comp _ _ _ _ _ _ _ _ _ _ f _ g) : category_scope.
65 (* this is like JMEq, but for the particular case of ~~; note it does not require any axioms! *)
66 Inductive heq_morphisms `{c:Category}{a b:c}(f:a~>b) : forall {a' b':c}, a'~>b' -> Prop :=
67 | heq_morphisms_intro : forall {f':a~>b}, eqv _ _ f f' -> @heq_morphisms _ _ c a b f a b f'.
68 Definition heq_morphisms_refl : forall `{c:Category} a b f, @heq_morphisms _ _ c a b f a b f.
69 intros; apply heq_morphisms_intro; reflexivity.
71 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.
72 refine(fun ob hom c a b f a' b' f' isd =>
74 | heq_morphisms_intro f''' z => @heq_morphisms_intro _ _ c _ _ f''' f _
77 Definition heq_morphisms_tran : forall `{C:Category} a b f a' b' f' a'' b'' f'',
78 @heq_morphisms _ _ C a b f a' b' f' ->
79 @heq_morphisms _ _ C a' b' f' a'' b'' f'' ->
80 @heq_morphisms _ _ C a b f a'' b'' f''.
83 apply heq_morphisms_intro.
89 Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:Category Ob Hom)(a b:Ob) : (hom a b) (eqv a b)
90 reflexivity proved by heq_morphisms_refl
91 symmetry proved by heq_morphisms_symm
92 transitivity proved by heq_morphisms_tran
93 as parametric_relation_heq_morphisms.
94 Add Parametric Morphism `(c:Category Ob Hom)(a b c:Ob) : (comp a b c)
95 with signature (eqv _ _ ==> eqv _ _ ==> eqv _ _) as parametric_morphism_comp.
99 Implicit Arguments heq_morphisms [Ob Hom c a b a' b'].
100 Hint Constructors heq_morphisms.
102 Definition EqualFunctors `{C1:Category}`{C2:Category}{F1obj}(F1:Functor C1 C2 F1obj){F2obj}(F2:Functor C1 C2 F2obj) :=
103 forall a b (f f':a~~{C1}~~>b), f~~f' -> heq_morphisms (F1 \ f) (F2 \ f').
104 Notation "f ~~~~ g" := (EqualFunctors f g) (at level 45).
106 Class IsomorphicCategories `(C:Category)`(D:Category) :=
109 ; ic_f : Functor C D ic_f_obj
110 ; ic_g : Functor D C ic_g_obj
111 ; ic_forward : ic_f >>>> ic_g ~~~~ functor_id C
112 ; ic_backward : ic_g >>>> ic_f ~~~~ functor_id D
115 (* this causes Coq to die: *)
116 (* Definition IsomorphicCategories := Isomorphic (CategoryOfCategories). *)