src/NaturalTransformations_ch7_4.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
   7 (*******************************************************************************)
   8 (* Chapter 7.4: Natural Transformations                                        *)
   9 (*******************************************************************************)
  10
  11 (* Definition 7.6 *)
  12 Structure NaturalTransformation `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}(F1:Functor C1 C2 Fobj1)(F2:Functor C1 C2 Fobj2) :=
  13 { nt_component : forall c:C1, (Fobj1 c) ~~{C2}~~> (Fobj2 c)
  14 ; nt_commutes  : forall `(f:A~>B), (nt_component A) >>> F2 \ f ~~ F1 \ f >>> (nt_component B)
  15 }.
  16 Notation "F ~~~> G" := (@NaturalTransformation _ _ _ _ _ _ _ _ F G) : category_scope.
  17 Coercion nt_component : NaturalTransformation >-> Funclass.
  18
  19 (* the identity natural transformation *)
  20 Definition nt_id `{C:Category}`{D:Category}{Fobj}(F:Functor C D Fobj) : NaturalTransformation F F.
  21   apply (@Build_NaturalTransformation _ _ _ _ _ _ _ _ F F (fun c => id (F c))).
  22   abstract (intros;
  23             setoid_rewrite left_identity;
  24             setoid_rewrite right_identity;
  25             reflexivity).
  26   Defined.
  27 Definition nt_comp `{C:Category}`{D:Category}
  28   {Fobj}{F:Functor C D Fobj}
  29   {Gobj}{G:Functor C D Gobj}
  30   {Hobj}{H:Functor C D Hobj}
  31   (nt_f_g:F ~~~> G) (nt_g_h:G ~~~> H) : F ~~~> H.
  32   apply (@Build_NaturalTransformation _ _ _ _ _ _ _ _ F H (fun c => nt_f_g c >>> nt_g_h c)).
  33   abstract (intros;
  34             set (@nt_commutes _ _ C _ _ D _ _ F G nt_f_g) as comm1;
  35             set (@nt_commutes _ _ C _ _ D _ _ G H nt_g_h) as comm2;
  36             setoid_rewrite    associativity;
  37             setoid_rewrite    comm2;
  38             setoid_rewrite <- associativity;
  39             setoid_rewrite <- comm1;
  40             reflexivity).
  41   Defined.
  42