src/Functors_ch1_4.v

   1 Generalizable All Variables.
   2 Require Import Notations.
   3 Require Import Categories_ch1_3.
   4
   5 (******************************************************************************)
   6 (* Chapter 1.4: Functors                                                      *)
   7 (******************************************************************************)
   8
   9 Class Functor
  10 `( c1                 : Category                               )
  11 `( c2                 : Category                               )
  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)
  18 }.
  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)
  26     (Fobj:C1->C2)
  27     (F:Functor C1 C2 Fobj)
  28     (a b:C1)
  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.
  32   Defined.
  33   Coercion functor_fobj : Functor >-> Funclass.
  34
  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.
  38   Defined.
  39
  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).
  43   intros; reflexivity.
  44   intros; reflexivity.
  45   intros; auto.
  46   Defined.
  47
  48 (* functors compose *)
  49 Definition functor_comp
  50   `(C1:Category)
  51   `(C2:Category)
  52   `(C3:Category)
  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)
  58    ].
  59   Defined.
  60 Notation "f >>>> g" := (@functor_comp _ _ _ _ _ _ _ _ _ _ f _ g)   : category_scope.
  61
  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)
  66   `(f:a~>b) :
  67   ((F1 >>>> F2) >>>> F3) \ f ~~ (F1 >>>> (F2 >>>> F3)) \ f.
  68   intros; simpl.
  69   reflexivity.
  70   Qed.
  71
  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.
  77   Qed.
  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 =>
  80     match isd with
  81       | heq_morphisms_intro f''' z => @heq_morphisms_intro _ _ c _ _ f''' f _
  82     end); symmetry; auto.
  83   Qed.
  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''.
  88   destruct 1.
  89   destruct 1.
  90   apply heq_morphisms_intro.
  91   setoid_rewrite <- H0.
  92   apply H.
  93   Qed.
  94
  95 (*
  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.
 103   auto.
 104   Defined.
 105 *)
 106 Implicit Arguments heq_morphisms [Ob Hom c a b a' b'].
 107 Hint Constructors heq_morphisms.
 108
 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).
 112
 113 Class IsomorphicCategories `(C:Category)`(D:Category) :=
 114 { ic_f_obj    : C -> D
 115 ; ic_g_obj    : D -> C
 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
 120 }.
 121
 122 (* this causes Coq to die: *)
 123 (* Definition IsomorphicCategories := Isomorphic (CategoryOfCategories). *)