1 Generalizable All Variables.
2 Require Import Preamble.
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.
64 (* this is like JMEq, but for the particular case of ~~; note it does not require any axioms! *)
65 Inductive heq_morphisms `{c:Category}{a b:c}(f:a~>b) : forall {a' b':c}, a'~>b' -> Prop :=
66 | heq_morphisms_intro : forall {f':a~>b}, eqv _ _ f f' -> @heq_morphisms _ _ c a b f a b f'.
67 Definition heq_morphisms_refl : forall `{c:Category} a b f, @heq_morphisms _ _ c a b f a b f.
68 intros; apply heq_morphisms_intro; reflexivity.
70 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.
71 refine(fun ob hom c a b f a' b' f' isd =>
73 | heq_morphisms_intro f''' z => @heq_morphisms_intro _ _ c _ _ f''' f _
76 Definition heq_morphisms_tran : forall `{C:Category} a b f a' b' f' a'' b'' f'',
77 @heq_morphisms _ _ C 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''.
82 apply heq_morphisms_intro.
88 Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:Category Ob Hom)(a b:Ob) : (hom a b) (eqv a b)
89 reflexivity proved by heq_morphisms_refl
90 symmetry proved by heq_morphisms_symm
91 transitivity proved by heq_morphisms_tran
92 as parametric_relation_heq_morphisms.
93 Add Parametric Morphism `(c:Category Ob Hom)(a b c:Ob) : (comp a b c)
94 with signature (eqv _ _ ==> eqv _ _ ==> eqv _ _) as parametric_morphism_comp.
98 Implicit Arguments heq_morphisms [Ob Hom c a b a' b'].
99 Hint Constructors heq_morphisms.
101 Definition EqualFunctors `{C1:Category}`{C2:Category}{F1obj}(F1:Functor C1 C2 F1obj){F2obj}(F2:Functor C1 C2 F2obj) :=
102 forall a b (f f':a~~{C1}~~>b), f~~f' -> heq_morphisms (F1 \ f) (F2 \ f').
103 Notation "f ~~~~ g" := (EqualFunctors f g) (at level 45).
105 Class IsomorphicCategories `(C:Category)`(D:Category) :=
108 ; ic_f : Functor C D ic_f_obj
109 ; ic_g : Functor D C ic_g_obj
110 ; ic_forward : ic_f >>>> ic_g ~~~~ functor_id C
111 ; ic_backward : ic_g >>>> ic_f ~~~~ functor_id D
114 (* this causes Coq to die: *)
115 (* Definition IsomorphicCategories := Isomorphic (CategoryOfCategories). *)