src/Functors_ch1_4.v

   1 Generalizable All Variables.
   2 Require Import Preamble.
   3 Require Import General.
   4 Require Import Categories_ch1_3.
   5
   6 (******************************************************************************)
   7 (* Chapter 1.4: Functors                                                      *)
   8 (******************************************************************************)
   9
  10 Class Functor
  11 `( c1                 : Category                               )
  12 `( c2                 : Category                               )
  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)
  19 }.
  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)
  27     (Fobj:C1->C2)
  28     (F:Functor C1 C2 Fobj)
  29     (a b:C1)
  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.
  33   Defined.
  34   Coercion functor_fobj : Functor >-> Funclass.
  35
  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.
  39   Defined.
  40
  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).
  44   intros; reflexivity.
  45   intros; reflexivity.
  46   intros; auto.
  47   Defined.
  48
  49 (* functors compose *)
  50 Definition functor_comp
  51   `(C1:Category)
  52   `(C2:Category)
  53   `(C3:Category)
  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)
  59    ].
  60   Defined.
  61 Notation "f >>>> g" := (@functor_comp _ _ _ _ _ _ _ _ _ _ f _ g)   : category_scope.
  62
  63
  64
  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.
  70   Qed.
  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 =>
  73     match isd with
  74       | heq_morphisms_intro f''' z => @heq_morphisms_intro _ _ c _ _ f''' f _
  75     end); symmetry; auto.
  76   Qed.
  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''.
  81   destruct 1.
  82   destruct 1.
  83   apply heq_morphisms_intro.
  84   setoid_rewrite <- H0.
  85   apply H.
  86   Qed.
  87
  88 (*
  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.
  96   auto.
  97   Defined.
  98 *)
  99 Implicit Arguments heq_morphisms [Ob Hom c a b a' b'].
 100 Hint Constructors heq_morphisms.
 101
 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).
 105
 106 (*
 107 Class IsomorphicCategories `(C:Category)`(D:Category){Fobj}{Gobj}(F:Functor C D Fobj)(G:Functor D C Gobj) :=
 108 { ic_forward  : F >>>> G ~~~~ functor_id C
 109 ; ic_backward : G >>>> F ~~~~ functor_id D
 110 }.
 111 *)
 112
 113 (* this causes Coq to die: *)
 114 (* Definition IsomorphicCategories := Isomorphic (CategoryOfCategories). *)