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
  63
  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.
  69   Qed.
  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 =>
  72     match isd with
  73       | heq_morphisms_intro f''' z => @heq_morphisms_intro _ _ c _ _ f''' f _
  74     end); symmetry; auto.
  75   Qed.
  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''.
  80   destruct 1.
  81   destruct 1.
  82   apply heq_morphisms_intro.
  83   setoid_rewrite <- H0.
  84   apply H.
  85   Qed.
  86
  87 (*
  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.
  95   auto.
  96   Defined.
  97 *)
  98 Implicit Arguments heq_morphisms [Ob Hom c a b a' b'].
  99 Hint Constructors heq_morphisms.
 100
 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).
 104
 105 Class IsomorphicCategories `(C:Category)`(D:Category) :=
 106 { ic_f_obj    : C -> D
 107 ; ic_g_obj    : D -> C
 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
 112 }.
 113
 114 (* this causes Coq to die: *)
 115 (* Definition IsomorphicCategories := Isomorphic (CategoryOfCategories). *)