src/FunctorCategories_ch7_7.v

   1 Generalizable All Variables.
   2 Require Import Notations.
   3 Require Import Categories_ch1_3.
   4 Require Import Functors_ch1_4.
   5 Require Import Isomorphisms_ch1_5.
   6 Require Import NaturalTransformations_ch7_4.
   7 Require Import NaturalIsomorphisms_ch7_5.
   8
   9 (*******************************************************************************)
  10 (* Chapter 7.5 and 7.7: Functor Categories                                     *)
  11 (*******************************************************************************)
  12
  13 (* Definition 7.9 *)
  14 Instance FunctorCategory `(C:Category)`(D:Category)
  15     : Category { Fobj : C->D & Functor C D Fobj } (fun F G => (projT2 F) ~~~> (projT2 G)) :=
  16 { id   := fun F                   => nt_id (projT2 F)
  17 ; comp := fun F G H nt_f_g nt_g_h => nt_comp nt_f_g nt_g_h
  18 ; eqv  := fun F G nt1 nt2         => forall c, (nt1 c) ~~ (nt2 c)
  19 }.
  20   intros.
  21    (apply Build_Equivalence;
  22             [ unfold Reflexive; unfold respectful; simpl; intros; reflexivity
  23             | unfold Symmetric; unfold respectful; simpl; intros; symmetry; auto
  24             | unfold Transitive; unfold respectful; simpl; intros; etransitivity; [ apply H | auto ] ]).
  25   abstract (intros; unfold Proper; unfold respectful; simpl; intros; setoid_rewrite H0; setoid_rewrite H; reflexivity).
  26   abstract (intros; simpl; apply left_identity).
  27   abstract (intros; simpl; apply right_identity).
  28   abstract (intros; simpl; apply associativity).
  29   Defined.
  30
  31 (* functors compose with each other, natural transformations compose with each other -- but you can also
  32  * compose a functor with a natural transformation! *)
  33 Definition LeftWhisker
  34   `{C:Category}`{D:Category}`{E:Category}
  35   {Fobj}{F:Functor C D Fobj}
  36   {Gobj}{G:Functor C D Gobj}
  37   (nat:F ~~~> G)
  38   {Hobj}(H:Functor D E Hobj) : ((F >>>> H) ~~~> (G >>>> H)).
  39   apply Build_NaturalTransformation with (nt_component:=(fun c => H \ (nat c))).
  40   abstract (intros;
  41             simpl;
  42             set (@nt_commutes _ _ _ _ _ _ F _ _ G nat) as nat';
  43             setoid_rewrite fmor_preserves_comp;
  44             setoid_rewrite <- nat';
  45             setoid_rewrite <- (fmor_preserves_comp H);
  46             reflexivity).
  47   Defined.
  48
  49 Definition RightWhisker
  50   `{C:Category}`{D:Category}`{E:Category}
  51   {Fobj}(F:Functor C D Fobj)
  52   {Gobj}{G:Functor D E Gobj}
  53   {Hobj}{H:Functor D E Hobj} : (G ~~~> H) -> ((F >>>> G) ~~~> (F >>>> H)).
  54   intro nat.
  55   apply Build_NaturalTransformation with (nt_component:=(fun c => (nat (F  c)))).
  56   abstract (intros;
  57             simpl;
  58             set (@nt_commutes _ _ _ _ _ _ G _ _ H nat) as nat';
  59             setoid_rewrite nat';
  60             reflexivity).
  61   Defined.
  62
  63 (* also sometimes called "horizontal composition" *)
  64 Definition GodementMultiplication
  65   `{A:Category}`{B:Category}`{C:Category}
  66   {F0obj}{F0:Functor A B F0obj}
  67   {F1obj}{F1:Functor A B F1obj}
  68   {G0obj}{G0:Functor B C G0obj}
  69   {G1obj}{G1:Functor B C G1obj}
  70   : (F0~~~>F1) -> (G0~~~>G1) -> ((F0 >>>> G0)~~~>(F1 >>>> G1)).
  71   intro phi.
  72   intro psi.
  73   apply Build_NaturalTransformation with (nt_component:=(fun (a:A) => G0 \ (phi a) >>> psi (F1 a))).
  74   abstract (intros;
  75             set (@nt_commutes _ _ _ _ _ _ F0 _ _ F1 phi) as comm1;
  76             set (@nt_commutes _ _ _ _ _ _ G0 _ _ G1 psi) as comm2;
  77             setoid_rewrite <- comm2;
  78             simpl;
  79             setoid_rewrite associativity;
  80             setoid_rewrite fmor_preserves_comp;
  81             setoid_rewrite comm1;
  82             setoid_rewrite <- fmor_preserves_comp;
  83             repeat setoid_rewrite <- associativity;
  84             apply comp_respects; try reflexivity;
  85             setoid_rewrite comm2;
  86             reflexivity).
  87   Defined.
  88   (* this operation is also a bifunctor from (FunctorCategory A B)*(FunctorCategory B C) to (FunctorCategory A C);
  89    * it is functorial *)
  90